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).