λProlog

Logic programming in higher-order logic

λProlog is a logic programming language based on an intuitionistic fragment of Church's Simple Theory of Types. Such a strong logical foundations provides λProlog with logically supported notions of

1. modular programming,
2. abstract datatypes,
3. higher-order programming, and
4. the lambda-tree syntax approach to the treatment of bound variables in syntax.

Implementations of λProlog contain implementations of the simply typed λ-terms as well as (of subsets) of higher-order unification.

Programming with Higher-Order Logic

This book by Dale Miller and Gopalan Nadathur focuses on how logic programming can exploit higher-order intuitionistic logic. The authors emphasize using higher-order logic programming to declaratively specify a range of applications. The book has its own web page. This book can be ordered on CUP, Amazon.com, Amazon.fr, and eBooks.

The Teyjus Implementation of λProlog System

Gopalan Nadathur and his team have developed the Teyjus implementation of λProlog. Version 2 is available for download. Its compiler is written in OCaml and it now supports separate computation, more effective uses of types at run-time, a restriction of unification to the higher-order pattern fragment, etc. The ALP Newsletter (March 2010) has an overview article about the Teyjus system.

An approach to reasoning about λProlog programs

Abella is an interactive theorem prover based on λ-tree syntax. This system is based on a two-level logic approach to reasoning about computation. The specification logic is used to specify computations: this logic is a subset of λProlog. The reasoning logic includes induction, co-induction, and the ∇-quantifier. Abella is well-suited for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding. The system has been designed and implemented by Andrew Gacek.

Parinati: Compiling Twelf signatures into λProlog

The dependently typed λ-calculus underlying Twelf can be effectively translated into the logic underlying λProlog in such a way that Teyjus can then preform proof search for Twelf. Zach Snow has written the system Parinati that implements this translation: as a result, Teyjus can be used to implement proof search in Twelf signatures.

Examples of Code

Various examples of λProlog code have been collected together into a small but growing collection. More updated examples can be found in the Teyjus distribution.

Language Documentation

Document of λProlog and its applications are available from a number of sources.

• Alwen Tui has course material on Programming in Higher-Order Logic.
• Amy Felty has written a tutorial on λProlog and its Applications to Theorem Proving (1997).
• Olivier Ridoux has written Lambda-Prolog de A à Z... ou presque (163 pages, French). Available as Postscript, PDF, and HTML).
• John Hannan has written a tutorial on Program Analysis in λProlog at the 1998 PLILP Conference.
• The FAQ is still preliminary, but a good place to start.
• There is a bibliography that includes papers on the theory, design, applications, and implementation of λProlog from between 1985 and 2000.

The lprolog mailing list

Gopalan Nadathur maintains the lprolog mailing list: visit https://wwws.cs.umn.edu/mm-cs/listinfo/lprolog to subscribe and to learn how to post. While this mailing list is mainly intended for the discussion of papers and systems concerning λProlog and related systems, announcements of conferences and workshops are also frequently posted there.