Fresh O'Caml: nominal abstract syntax for the masses.
2005 ACM SIGPLAN Workshop on ML.
Nominal abstract syntax, as pioneered by the `FreshML' series of metalanguages, provides first-order tools for the representation and manipulation of syntax involving bound names, binding operations and alpha-equivalence. Fresh O'Caml fuses nominal abstract syntax with the full Objective Caml language to yield a functional programming language with powerful facilities for representing and manipulating syntax. In this paper, we first provide an examples-driven overview of the language and its functionality. Then we proceed to comment on some of the difficult issues involved in implementing nominal abstract syntax and explain how they have been addressed in the latest version of the compiler.
Fresh Objective Caml user manual.
With Andrew Pitts. University of Cambridge Computer Laboratory Technical Report 621, February 2005.
The Fresh Approach: functional programming with names and binders.
PhD thesis, University of Cambridge Computer Laboratory, February 2005.
This thesis concerns the development of a language called Fresh Objective Caml, which is an extension of the Objective Caml language. It provides for the manipulation of syntactic structures involving alpha-convertible names and binding operations.
After an introductory chapter which includes a survey of related work, we describe the Fresh Objective Caml language in detail. We next proceed to formalise a small core language which captures its essence: we call this Mini-FreshML. We provide two varieties of operational semantics for this language and prove them equivalent. Then in order to prove correctness properties of representations of syntax in the language we introduce a new variety of domain theory called FM-domain theory, based on the permutation model of name binding of Pitts and Gabbay. We show how classical domain-theoretic constructions---including those for the solution of recursive domain equations---fall naturally into this setting, where they are augmented by new constructions to handle name-binding.
After developing the necessary domain theory, we demonstrate how it may be used to give a monadic denotational semantics to Mini-FreshML. This semantics in itself is quite novel and demonstrates how a simple monad of continuations is sufficient to model dynamic allocation of names. We prove that our denotational semantics is computationally adequate with respect to the operational semantics---in other words, equality of denotation implies observational equivalence. We then show how the denotational semantics may be used to prove our desired correctness properties.
In the penultimate chapter, we examine the Fresh O'Caml implementation itself, describing detailed issues in the compiler and runtime system. Then in the final chapter we provide an assessment of the work completed so far together with a discussion of future avenues of research.
Download: PDF. The thesis is also available in a more compact form as a Computer Laboratory Technical Report.
On a Monadic Semantics for Freshness.
With Andrew Pitts. Theoretical Computer Science, to appear. An earlier, shorter version was presented at APPSEM 2004.
A standard monad of continuations, when constructed with domains in the world of FM-sets, is shown to provide a model of dynamic allocation of fresh names that is both simple and useful. In particular, it is used to give the first correct proof of the fact that the powerful facilities for manipulating fresh names and binding operations provided by the `FreshML' series of metalanguages respect alpha-equivalence of object-level languages up to meta-level contextual equivalence.
Swapping the Atom: Programming with Binders in Fresh O'Caml.
Presented at MERLIN 2003.
We describe Fresh O'Caml, a metalanguage designed to correctly manipulate object-level syntax involving alpha-convertible names and binding operations. The language extensions made to Objective Caml are surveyed from a practical perspective and the implementation details are briefly discussed.
FreshML: Programming with Binders Made Simple.
With Andrew Pitts and Jamie Gabbay. Presented at ICFP'03.
FreshML extends ML with elegant and practical constructs for declaring and manipulating syntactical data involving binding operations. User-declared FreshML datatypes involving binders are concrete, in the sense that values of these types can be deconstructed by matching against patterns naming bound variables explicitly. Such matching may have a computational effect in which bound names get swapped with freshly generated names. Previous work on FreshML used a complicated static type system inferring information about the "freshness" of names for expressions in order to tame such effects. The main contribution of this paper is to show (perhaps surprisingly) that a much simpler type system without freshness inference, coupled with name swapping and a conventional treatment of fresh name generation, suffices for FreshML's crucial correctness property---namely that values of datatypes involving binders are operationally equivalent if and only if they represent alpha-equivalent pieces of object-level syntax. This correctness result is established via a novel denotational semantics. FreshML without static freshness inference is no more impure than ML and our experiences programming in it show that it supports a programming style pleasingly close to informal practice when it comes to dealing with syntax modulo alpha-equivalence.
Download: PDF. Please also note the erratum to this paper.
The Implementation of FreshML.
Project dissertation for Part II of the Cambridge University Computer Science Tripos, 2000.
Last update 7th August 2005.