λ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 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 and can be ordered from 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. Probably the most elegant formalized meta theory for the π-calculus is the one done using Abella. The system was originally implemented by Andrew Gacek: more recent updates have been contributed by Kaustuv Chaudhuri and Yuting Wang.

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

Examples of λProlog code can be found various places: in the Teyjus distribution; in an extraction from the book Programming with Higher-Order Logic; and in a small collection.

Language Documentation

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

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.


Last updated: 10 September 2013.