Lawrence C. Paulson
18 works on record
Works
Isabelle
1994
ML for the working programmer
1991
Logic and computation
1987
Isabelle/HOL
The foundation of a generic theorem prover
1988
Rewriting in Cambridge LCF
1987
The representation of logics in higher-order logic
1987
Proving termination of normalization functions for conditional expressions
1985
Natural deduction theorem proving via higher-order resolution
1985
Interactive theorem proving with Cambridge LCF
1985
Natural deduction proof as higher-order resolution
1985
Lessons learned from LCF
1984
Constructing recursions operators in intuitionistic type theory
1984
Verifying the unification algorithm in LCF
1984
Recent developments in LCF
1983
Tactics and tacticals in Cambridge LCF
1983
The revised logic PPLamda a reference manual
1983
Mechanized proofs of security protocols