Examples of Teyjus (Lambda Prolog) Programs

As a language, Lambda Prolog contains some capabilities previously unknown to programming. Exploiting the language properly therefore involves understanding how to use the novel features wisely and to real advantage. Much literature is now available on doing this. The examples accessible from this page do not pretend to replace this literature. Rather, they are intended to familiarize you with the basic structure of programming in Lambda Prolog, especially emphasizing the use of the Teyjus version of this language, to introduce some of the new capabilities and to provide you with relevant pointers to the literature on the use of Lambda Prolog.

If you have interesting examples of Lambda Prolog use to contribute, we would be glad to have them. Please format these in a manner that you think best brings out the important concepts, put all the material in one directory linking to it from an index.html file and send a tarred version of the directory to gopalan@cs.uchicago.edu. Of course, please make sure that your programs actually run under Teyjus and that your Web material `works' before sending these on!

Representing and Manipulating Formulas, based on material in Higher-Order Logic Programming by Gopalan Nadathur and Dale Miller.

Representing and Manipulating Programs, based on material in Higher-Order Logic Programming by Gopalan Nadathur and Dale Miller.

An interactive theorem prover implemented in Lambda Prolog, adapted from work done by Amy Felty.

Implementations of logic programming languages:
- An ordered linear logic programming language, developed by Jeff Polakow.
- A linear logic programming language, also due to Jeff Polakow.

Last changed by gopalan@cs.umn.edu on April 9, 2004