What is Pure FreshML?
Pure FreshML is a prototype implementation of the programming language
described in the paper Static Name Control for FreshML.
Here is the source code. This is an early prototype,
without documentation; it is provided only as a means of reproducing the experiments
described in the paper. It requires OCaml and
a SAT solver (by default, relsat, but zchaff can also be used).
Installation requires omake. A more polished prototype, with a simpler
installation process, will be made available in the future.
Here are some sample code fragments that might be of interest:
- Conversion to A-normal form, in direct style (anf-direct.fml);
this algorithm, explained in the paper, uses explicit, name-capturing contexts;
- Conversion to A-normal form, in continuation-passing style (anf.fml);
this algorithm uses (defunctionalized) continuations, and gives rise to fewer proof obligations;
- Sets of atoms, implemented as lists of distinct atoms
(atomlist.fml);
- An interpreter for a lambda-calculus with callcc
(callcc.fml);
- Closure conversion
(cc.fml); this algorithm requires fine-grained assertions;
- Hoisting
(hoist.fml); this follows closure conversion, and is
somewhat remarkable because it does not require much ingenuity; (imagine
doing this with de Bruijn indices!);
- Conversion from lambda-calculus to combinators
(comb.fml);
- CPS conversion
(cps.fml);
- Conversion from de Bruijn notation to nominal notation
(debruijn.fml);
- An interpreter for a lambda-calculus with pattern matching
(interpreter.fml);
- An interpreter for MetaML
(metaml.fml);
- Normalization by evaluation, as described in my paper
(nbe.fml) or with delayed computations
(nbe-delayed.fml);
- Type-directed normalization by evaluation
(typed-nbe.fml).
