Author: Tobias Nipkow
Copyright 1992 University of Cambridge
Logic for Computable Functions.
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.