CoRR, January 1993

• Lawrence C. Paulson:
  Verifying the Unification Algorithm in LCF.
  
• Lawrence C. Paulson:
  Constructing Recursion Operators in Intuitionistic Type Theory.
  
• Lawrence C. Paulson:
  Proving Termination of Normalization Functions for Conditional Expressions.
  
• Lawrence C. Paulson:
  Natural Deduction as Higher-Order Resolution.
  
• Lawrence C. Paulson:
  The Foundation of a Generic Theorem Prover.
  
• Lawrence C. Paulson:
  Isabelle: The Next 700 Theorem Provers.
  
• Lawrence C. Paulson:
  A Formulation of the Simple Theory of Types (for Isabelle).
  
• Lawrence C. Paulson:
  A Higher-Order Implementation of Rewriting.
  
• Lawrence C. Paulson, Andrew W. Smith:
  Logic Programming, Functional Programming, and Inductive Definitions.
  
• Lawrence C. Paulson:
  Designing a Theorem Prover.
  

Last update Thu May 23 18:31:03 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page