The FreshML research project investigated methods in functional programming for manipulating syntax involving α-convertible names and binding operations, based on the permutation model of name binding pioneered by Pitts and Gabbay.

The project, which started in 2001 and finished at the end of 2004, was funded by EPSRC grant GR/R07615/1 and a donation from Microsoft Research Cambridge. It was led by Andrew Pitts and employed Jamie Gabbay, Mark Shinwell and Peter White (graduate intern) at Cambridge University. There was collaboration with Mike Gordon and Christian Urban at Cambridge University, Simon Peyton Jones and Nick Benton at Microsoft Research Cambridge, and James Cheney visiting from Cornell University.

Some of the main achievements of the project were:

• Nominal sets - a simplified presentation of the Gabbay-Pitts model of names and binding, together with first- and higher-order logics of nominal sets.
• Fresh Objective Caml - a patch of the Objective Caml language that includes facilities for programming with names and binders.
• Domain theory in nominal sets with applications to the denotational semantics of dynamically allocated names, including a detailed proof of correctness of Fresh Objective Caml's representation of syntax modulo α-equivalence.
• Nominal unification - a new form of unification for syntax modulo α-equivalence, with applications to logic programming.

On this web site you can find:

• a list of publications that resulted from work done by the project;
• the final report on the research project (pdf, 122KB);
• how to typeset the "freshness quantifier" in LaTeX.

Software:

• Fresh Objective Caml web site

Links:

• Christian Urban's Isabelle theory files for nominal unification;
• James Cheney's implementation of AlphaProlog, a logic programming language with names and binding based on nominal unification.