Lambda is a program for solving lambda definability problems of order
at most two.
The Lambda distribution consists of:
- The PDF for the paper
Mechanizing logical relations,
which describes the theory on which Lambda is based and explains what
the program does.
- A short manual page describing Lambda.
- The implementation of Lambda. Lambda is written in ANSI C, with
the exception of its lexical analyzer and parser, which are written in
Lex (Flex) and Yacc (Bison) source, respectively. It uses one UNIX
System V system call. The C programs that it generates also conform
to the ANSI standard; they use several UNIX System V system calls in
order to implement checkpointing. The makefile that is included with
the distribution is set up to use GCC, the GNU C Compiler, but can be
easily changed to use another ANSI C Compiler. Also, the makefile is
set up to use Flex and Bison, but can be easily changed to use Lex and
- A number of example lambda definability problems, together with
To obtain a copy of the distribution: