Papers on (Co)Induction and (Co)Recursion

People expect a proof assistant to support definition by recursion, but deriving recursion from fundamental logical principles is surprisingly difficult. Only recently could we say that support for recursive datatype and function definitions in proof assistants is starting to be good enough to support the main idioms of functional programming.

Inductive definitions are fundamental in mathematics and during the 1990s became increasingly prominent in proof assistants as well. The well-known inductive method for verifying security protocols in Isabelle only became possible because of the work described in papers such as those below.

  1. L. C. Paulson.
    Deriving Structural Induction in LCF. In: G. Kahn, D. B. MacQueen, G. Plotkin, editors, Semantics of Data Types (Springer, 1984), 197–214.
  2. L. C. Paulson.
    Proving termination of normalization functions for conditional expressions. J. Automated Reasoning 2 (1986), 63–74.
  3. L. C. Paulson.
    Constructing recursion operators in Intuitionistic Type Theory. J. Symbolic Computation 2 (1986), 325–355.
  4. L. C. Paulson.
    Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
  5. L. C. Paulson.
    Mechanizing coinduction and corecursion in higher-order logic. J. Logic and Computation 7 (March 1997), 175–204.
  6. L. C. Paulson.
    Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
  7. L. C. Paulson.
    A fixedpoint approach to (co)inductive and (co)datatype definitions In: G. Plotkin, C. Stirling, and M. Tofte (editors), Proof, Language, and Interaction: Essays in Honour of Robin Milner (MIT Press, 2000), 187–211.
  8. L. C. Paulson.
    A simple formalization and proof for the mutilated chess board.
    Logic J. of the IGPL 9 3 (2001), 499–509.

Last revised: 23 February, 2015

Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge