Skip to main content Accessibility help
×
Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-05T01:43:29.756Z Has data issue: false hasContentIssue false

1 - Survey and History of LCF

Published online by Cambridge University Press:  17 September 2009

Lawrence C. Paulson
Affiliation:
University of Cambridge
Get access

Summary

Cambridge LCF is an interactive theorem prover for reasoning about computable functions. The terms of its logic, PPλ, constitute a tiny functional programming language. Cambridge LCF can be used for experimenting with first order proof; studying abstract constructions in domain theory; comparing the denotational semantics of programming languages; and verifying functional programs. It can reason about both strict and lazy evaluation.

There are many theorem provers in the LCF family. Each is descended from Edinburgh LCF and retains its fundamental ideas:

  • The user interacts with the prover through a programmable meta language, ML.

  • Logical formulae, theorems, rules, and proof strategies are ML data.

  • The prover guarantees soundness: it checks each inference and records each assumption.

Edinburgh LCF was developed in order to experiment with Scott's Logic of Computable Functions [41]. It performed many proofs involving denotational semantics and functional programming.

Cambridge LCF extended the logic of Edinburgh LCF with ∨, ∃, ⇔, and predicates, improved the efficiency, and added several inference mechanisms. It has been used in proofs about functional programming and several other theorem provers have been built from it.

LCF_LSM was developed for reasoning about digital circuits in a formalism related to CCS [32]. It verified some realistic devices [39], but is now obsolete.

HOL supports Church's Higher Order Logic [37], a general mathematical formalism. It is mainly used to prove digital circuits correct.

Another system supports a higher order Calculus of Constructions that can represent many other calculi.

Type
Chapter
Information
Logic and Computation
Interactive Proof with Cambridge LCF
, pp. 3 - 12
Publisher: Cambridge University Press
Print publication year: 1987

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×