Peter Selinger: Lambda-Mu-Nu Calculus Compiler

An Implementation of the Lambda-Mu-Nu Calculus

The lambda-mu-nu calculus is an extension of Parigot's lambda-mu calculus with disjunction types. It was proposed by Pym and Ritter. A syntactic variant of this calculus is described in my paper "Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus".

This is an experimental compiler for the call-by-name lambda-mu calculus with disjunction, based on a Krivine-style abstract machine. The abstract machine is in turns derived from the CPS semantics that is given in my paper. A detailed description of the compiler, the abstract machine, and the underlying CPS semantics can be found in the documentation.

The input to the compiler is abstract syntax - we do no typechecking, but the correctness of the implementation depends on the typability of the source. Parser and typechecker can be added later. The execution of the underlying abstract machine can be observed step by step by starting the compiled program with the -v option. The target language is C, with a set of runtime primitives defined in runtime.c.

Usage:

To load the compiler, type

    use
"compiler.sml";

from SML,
include "compiler.ml";; from Caml Light, or

    #use
"compiler.oml";;

from Objective Caml.
Then, type

    compile term
"myfile.c";;

to generate a C-program from a term. Compile this with

    gcc myfile.c -o
myfile

from a shell. Make sure that the file runtime.c is in the path for files to be included. Finally, execute the code via
myfile [-v]
The -v tag causes the program to print information on each step of the computation.

Distribution:

README: this file (3 kB)
compiler.sml: the compiler, SML (19 kB)
compiler.ml: the compiler, Caml Light (19 kB)
compiler.oml: the compiler, Objective Caml (19 kB)
runtime.c: the runtime system (3 kB)
lammunu.dvi.gz: the documentation, dvi (23 kB)
lammunu.pdf.gz: the documentation, pdf (72 kB)
lammunu.ps.gz: the documentation, postscript (52 kB)

Or get them all at once as lammunu.tar.gz (158 kB).

Version History:

Version 1.1 (07/20/98): first public release.
Version 1.3 (08/19/98): added support for basic constants and functions.

License:

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 1, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

Back to Homepage:

Peter Selinger / Department of Mathematics and Statistics / Dalhousie University
selinger@mathstat.dal.ca / PGP key / PGP key

Updated Feb 22, 1999