User loginNavigation |
Proofs and puddings -- or, how pure is the pure lambda calculus, pt 3In 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 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. By Lucius Gregory Meredith at 2007-01-08 22:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 4734 reads
|
Browse archives
Active forum topics |
Recent comments
27 weeks 2 days ago
27 weeks 2 days ago
27 weeks 2 days ago
49 weeks 3 days ago
1 year 1 week ago
1 year 3 weeks ago
1 year 3 weeks ago
1 year 5 weeks ago
1 year 10 weeks ago
1 year 10 weeks ago