Logic programming

From The Twelf Project

Most of the articles and examples on this wiki are focused towards using Twelf as a specification langauge, 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.

[edit] 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].

[edit] See also

• Logic Programming in the User's Guide
• Logic programming at Wikipedia

[edit] References

1. ↑ Karl Crary - Toward a Foundational Typed Assembly Language
   

   2003 Symposium on Principles of Programming Languages , 2003

   Bibtex

   Author : Karl Crary
   Title : Toward a Foundational Typed Assembly Language
   In : 2003 Symposium on Principles of Programming Languages -
   Address :
   Date : 2003
   

2. ↑ Andrew W. Appel, Amy P. Felty - Dependent Types Ensure Partial Correctness of Theorem Provers
   

   Journal of Functional Programming 14(1):3--19, January, 2004

   Bibtex

   Author : Andrew W. Appel, Amy P. Felty
   Title : Dependent Types Ensure Partial Correctness of Theorem Provers
   In : Journal of Functional Programming -
   Address :
   Date : January 2004