Lawrence C. Paulson

Isabelle/HOL

Logic and Computation

Constructing recursions operators in intuitionistic type theory

1984

The foundation of a generic theorem prover

1988

Interactive theorem proving with Cambridge LCF

1985

Lessons learned from LCF

1984

Mechanized proofs of security protocols

Natural deduction proof as higher-order resolution

1985

Natural deduction theorem proving via higher-order resolution

1985

Proving termination of normalization functions for conditional expressions

1985

Recent developments in LCF

1983

The representation of logics in higher-order logic

1987

The revised logic PPLamda a reference manual

1983

Rewriting in Cambridge LCF

1987

Tactics and tacticals in Cambridge LCF

1983

Verifying the unification algorithm in LCF

1984

Logic and computation

1987

ML for the working programmer

1991

Isabelle

1994