Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications of Lawrence C Paulson
[go: Go Back, main page]

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.