Papers on (Co)Induction and (Co)Recursion

Also see papers on Verifying Security Protocols

1. Deriving Structural Induction in LCF. In: G. Kahn, D. B. MacQueen, G. Plotkin, editors, Semantics of Data Types (Springer, 1984), 197–214.
2. Proving termination of normalization functions for conditional expressions. J. Automated Reasoning 2 (1986), 63–74.
3. Constructing recursion operators in Intuitionistic Type Theory. J. Symbolic Computation 2 (1986), 325–355.
4. Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
5. Mechanizing coinduction and corecursion in higher-order logic. J. Logic and Computation 7 (March 1997), 175–204.
6. Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
7. 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. A Simple Formalization and Proof for the Mutilated Chess Board.
   Logic J. of the IGPL 9 3 (2001), 499–509.