LCF theorem prover

Embed this Topic
LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general-purpose programming language ML to allow users to write theorem-proving tactics. Theorems in the system are propositions of a special "theorem" abstract datatype. The ML type system ensures that theorems are derived using only the inference rules given by the... more
Read article at Wikipedia

Facts from the Community

From the Proofs are Programs base

How it applied the concept:

  • ML/LCF exploited two central features of functional languages, higher-order functions and types. A proof tactic is a function taking a goal formula to be proved and returning a list of subgoals paired with a justification. A justification, in turn, is a function from proofs of the subgoals to a proof of the goal. A tactical is a function that combined small tactics into larger tactics. The type system was a great boon in managing the resulting nesting of functions that return functions that accept functions.
top ↑

Similar topics in Freebase

  • Haskell

    Haskell

    Haskell (pronounced [ˈhæskəl]) is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. Following the release of Miranda by Research Software Ltd, in 1985, interest in lazy functional...
  • Java

    Java

    Java refers to a number of computer software products and specifications from Sun Microsystems that together provide a system for developing application software and deploying it in a cross-platform environment. Java is used in a wide variety of computing platforms from embedded devices and mobile...
  • Lisp

    Lisp

    Lisp (or LISP) is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the second-oldest high-level programming language in widespread use today; only Fortran is older. Like Fortran, Lisp has changed a...
  • Objective Caml

    Objective Caml

    Objective Caml, or OCaml (pronounced /oʊˈkæməl/ oh-KAM-əl) is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996. OCaml is an open source project managed and principally maintained by INRIA. OCaml...
  • Miranda

    Miranda

    Miranda is a non-strict purely functional programming language designed by David Turner as a successor to his earlier programming languages SASL and KRC, using some concepts from ML and Hope. It was produced by Research Software Ltd. of England (which holds a trademark on the name Miranda) and was...
  • Coq

    Coq

    In computer science, Coq is a proof assistant application. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the...

These people have edited this topic:

  • warren
Edit this topic
Edit and Show details

Add or delete facts, download data in JSON or RDF formats, and explore topic metadata.

Freebase Logo
What is Freebase?

Freebase is a huge collection of facts, built by people like you. Freebase connects facts in ways other sites can't, giving you new ways to explore millions of subjects.
You can help improve it!

Freebase Attribution

Freebase data is free for use under the CC-BY license.

The original description for LCF theorem prover was automatically generated from Wikipedia.org licensed under the GNU Free Documentation License.
[1]
Learn more about Freebase licensing and attribution