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: an Axiomatic Approach to the Semantics of Control in Functional Languages". 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. 7/13/98-8/19/98. Copyright 1998 Peter Selinger. Version 1.3. 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: From ftp://ftp.cis.upenn.edu/pub/papers/selinger/lammunu/: * 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. _________________________________________________________________ Peter Selinger / Department of Mathematics / University of Michigan selinger@umich.edu Updated Feb 22, 1999