Some Program Manipulating Programs in Teyjus

The code accessible from this page illustrates the use of higher-order abstract syntax as it is supported in Lambda Prolog in representing and manipulating programs in a simple (functional) programming language. One component to understand here is the way programs are represented. Four manipulation tasks are also considered and these illustrate the benefits of beta reduction in realizing substitution into formulas, of higher-order unification in probing formula structure and of the new scoping primitives in Lambda Prolog in carrying out computations over abstraction structure. The menu below provides some help in understanding the structure of the code.

Term encodings for programs in a functional programming language
- Kinds and constants for encoding function structure (abstraction and application)
- Constants representing programming language primitives
- Encodings of some simple programs
- Signature and code for a recognizer for valid program terms
Implementing an interpreter for the programming language
- Signature and code for an evaluator for the `pure' terms
- Signature and code for an evaluator for the full programming language
- Signature and code for a testing harness
- Script depicting a run of the code
An example of program analysis using higher-order unification
- Signature and code for performing a currying transformation on binary functions
- Signature and code for a testing harness
- Script depicting a run of the code
Another example of program analysis using higher-order unification
- Signature and code for recognizing tail recursiveness of binary functions
- Signature and code for a testing harness
- Script depicting a run of the code
A final example of program analysis, this time using scoping primitives for recursion over abstraction structure
- Signature and code for a tail recursion recognizer for arbitrary arity functions
- Signature and code for a testing harness
- Script illustrating the use of the code
Download a tarred version of all the code

The code in this directory is based on the paper ``Higher-Order Logic Programming'' by Gopalan Nadathur and Dale Miller

Last changed by gopalan@cs.umn.edu on August 12, 2003