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.
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T211851 by the dblp team