Logic programming
Most of the articles and examples on this wiki are focused towards using Twelf as a specification language, useful for encoding an object logic and then stating and proving metatheorems about that object logic. However, Twelf originated from Elf, and like Elf it is a dependently-typed, higher-order logic programming language based on the logic LF.
A Twelf signature may contain, among other things, some type family declarations and some constants inhabiting those type families. A logic programming language takes a type as an input, and it then uses a simple search strategy to try and discover a term that has that type using the constants that have been defined. By the judgments as types principle, this means that Twelf is searching for a derivation - a proof witness - of a particular judgment.
Twelf's logic programming engine is activated by %solve and %query directives. It can also be activated directly inside ML; see the section on interactive queries in the User's Guide for more information. Twelf's tabled logic programming engine is activated by the %querytabled directive.
Uses of logic programming in Twelf
- Implementing a reference typechecker/evaluator - If the static and dynamic semantics of a programming language are written correctly, then the specification of the static semantics can be . This was a component to the The POPLmark Challenge challenge; the case study of a language with references, among other examples, demonstarte Twelf in this capacity.
- Writing programs and then proving things about them: The TALT project ^{[1]} includes a code checker written as a Twelf logic program, along with a proof in Twelf that code that passes the checker is safe according to a safety policy.
- Tactical theorem proving - in the style described by Appel and Felty in ^{[2]}.
See also
- Logic Programming in the User's Guide
- Logic programming at Wikipedia
References
- ↑
Karl Crary - Toward a Foundational Typed Assembly Language
- 2003 Symposium on Principles of Programming Languages ,2003
- BibtexAuthor : Karl Crary
Title : Toward a Foundational Typed Assembly Language
In : 2003 Symposium on Principles of Programming Languages -
Address :
Date : 2003
- ↑
Andrew W. Appel, Amy P. Felty - Dependent Types Ensure Partial Correctness of Theorem Provers
- Journal of Functional Programming 14(1):3--19, January 2004
- BibtexAuthor : Andrew W. Appel, Amy P. Felty
Title : Dependent Types Ensure Partial Correctness of Theorem Provers
In : Journal of Functional Programming -
Address :
Date : January 2004