λ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 modular programming, abstract datatypes, higher-order programming, and 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.
Zakaria Chihani in producing a series of video tutorials providing an introduction to λProlog and to higher-order logic programming.
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 and can be ordered from CUP, Amazon.com, Amazon.fr, and eBooks. |
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. |
ELPI |
Claudio Sacerdoti Coen and Enrico Tassi have lead a team that developed ELPI: an embeddable, λProlog interpreter. The interpreter is written in OCaml and is available online. The system is described in a paper that appeared LPAR 2015. |
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. |
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 λ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.
Document of λProlog and its applications are available from a number of sources.
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.