• The first line declares the name of the module, using the module directive.
• A module may import or accumulate other modules. These are declared using the import and accumulate directives. The scope of a constant can be restricted to this module using the local and localkind directive.
• Declarations are used to attribute lexical and typing information to constants: they are declared using the directives kind, type, infix, infixl, and infixr. These declarations must appear prior to the place where the constants they declare are used.
• Program clauses, represented by logical formulas, are the fourth major component of a module.

Notice that all the declarations in a module are considered global to that module, even if they do not occur at the front of the module. Comments are also allowed: % mark a comment that extends to the end of the line and %( and )% bracket comments.

Examples of modules are available below. The first few examples are rather small and straightforward. Most of the remaining ones are more elaborate. Thanks to all who have provided links to their contributations.

1. System modules of Terzo 1.0b.

2. Higher-order programming. Quantification over predicates and functions in simple higher-order Horn clause programs is illustrated here.

3. Higher-order unification. The unification of simply typed lambda-terms is illustrated here.

4. Utilities. Some simple and useful utilities are presented.

5. Specification for the pi-calculus. Specification follows the presentation in the early papers on the pi-calculus, in particular, in Modal Logics for Mobile Processes by Milner, Parrow, and Walker.

6. An interpreter for Lolli. This is based on the linear logic programming language described in following paper: Logic Programming in a Fragment of Intuitionistic Linear Logic, by Joshua S. Hodas and Dale Miller. Information and Computation, Vol. 110, No. 2, May 1, 1994, pp. 327-365. (Abstract) (BibTeX Entry) (DVI) (Postscript) (Reprints by request)

7. Tactics for theorem proving. This specifications of tactics is based on code published in the following paper: Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language, by Amy Felty. Journal of Automated Reasoning, 11(1):43-81, August 1993. (See her web page for the paper.)

8. A simple theorem prover for intuitionistic sequent calculus. This specification of the theorem prover follows a specification also given by Amy Felty in the paper mentioned above. See also her Lambda Prolog code for specifying and implementing theorem provers

9. Alan Smaill and Claudio Castellini have written a lambda Prolog tactic theorem prover for first-order temporial logic. More information on this recent system can be found on the web.

10. Giorgio Delzanno at the University of Genoa has written in lambda Prolog a interpreter for Yahoo, an object-orient language. The lambda Prolog source code is available.

11. lambda Clam is a tool for automated theorem proving in higher order domains. This system is written using the Prolog/MALI implementation of lambda Prolog.

12. Markus Mottl has implemented in the Teyjus implementation of lambda Prolog a program transformation framework for a pure and strict functional language.

13. Chuck Liang has implemented in the Teyjus implementation of lambda Prolog a compiler for an imperative programming language, outputing source code for the Sparc architecture. This work is part of an ongoing project to use higher order abstract syntax and higher order logic programming for compiler implementation. Chuck has also implemented a parser generator in Teyjus.