Lambda the Ultimate

In http://lambda-the-ultimate.org/node/1930 and http://lambda-the-ultimate.org/node/1944 i described a lambda calculus with quotation and a program logic. Ever the one to believe that theory and practice should verify each other, i have put together, here (http://svn.biosimilarity.com/src/rlambda/), a first draft implementation of the ideas in OCaml.

Currently, the system supports a very brittle command line REPL for a pretty raw syntax. The main point of interest is that the code is factored more or less along the lines of the specification, making use of recursive modules. That is, syntax and structural equivalence are functors of a module type IDENTIFIER. Then a reflective module is made by interpreting the IDENTIFER operations using terms. See the code. (Note: i wanted to have the operational semantics module also be a functor and recursively instantiate, but i couldn't get the OCaml compiler to get the three-level functor to work properly. Email me at lgreg.meredith@biosimilarity.com for further discussion.)

In an upcoming update i will add a simplistic model-checker for the logic.

System requirements

i have only tested the code on Mac OS X (tiger) using "OCamlDuce version 3.09.2pl2", but i'm pretty sure that a plain vanilla version of OCaml at or around version 3.09.x should build and run the code. The make files are written for

lgmaclt:~/work/src/projex/biosimilarity/reflection/rlambda/ocaml lgm$ `which make` --version
GNU Make 3.80
Copyright (C) 2002 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.
lgmaclt:~/work/src/projex/biosimilarity/reflection/rlambda/ocaml lgm$

Copyright

The source files say Copyright: Biosimilarity LLC. All rights reserved. But, everything on the site is under GPL. So, you are free to do what you want with the code -- such as it is -- as long as you respect GPL.