Lessons learned from LCF: A Survey of Natural Deduction Proofs

Open Access
Publisher Website
Google Scholar
Abstract
The LCF project has produced a family of interactive, programmable theorem-provers, particularly intended for verifying computer hardware and software. The introduction sketches basic concepts: the metalanguage ML, the logic PPLAMBDA, backwards proof, rewriting, and theory construction. A historical section surveys some LCF proofs. Several proofs involve denotational semantics, notably for compiler correctness. Functional programs for parsing and unification have been verified. Digital circuits have been proved correct, and some subsequently fabricated. There is an extensive bibliography of work related to LCF. The most dynamic issues at present are data types, subgoaling techniques, logics of computation, and the development of ML.

This publication has 0 references indexed in Scilit: