λ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 (subsets) of higher-order unification.
Document of λProlog and its applications are available from a number of sources.
Abella is an interactive theorem prover based on a number of new ways to exploit inductive and coinductive reasoning with relations. Abella is well-suited for reasoning about specification that manipulate objects with binding since it contains the following three logically motivated features: (1) direct support of λ-tree syntax (sometimes also called HOAS); (2) the ∇-quantifier; and (3) a built-in, two-level logic approach to reasoning about computation. In the latter feature, the specification logic is used to specify computations: this logic is a subset of λProlog. Abella's logic then serves as the reasoning logic. Probably the most elegant formalization of the π-calculus and its meta-theory is the one written in Abella. Principle contributors to the implementaiton of Abella are Kaustuv Chaudhuri, Andrew Gacek, and Yuting Wang.
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.
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.