Department of Computer Science and Technology

Technical reports

The Fresh Approach: functional programming with names and binders

Mark R. Shinwell

February 2005, 111 pages

This technical report is based on a dissertation submitted December 2004 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Queens’ College.

DOI: 10.48456/tr-618

Abstract

This report concerns the development of a language called Fresh Objective Caml, which is an extension of the Objective Caml language providing facilities for the manipulation of data structures representing syntax involving α-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. Next, we proceed to formalise a small core language which captures the essence of Fresh Objective Caml; 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 from 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 exploited 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. After this, we show how the denotational semantics may be used to prove our desired correctness properties.

In the penultimate chapter, we examine the implementation of Fresh Objective Caml, describing detailed issues in the compiler and runtime systems. Then in the final chapter we close the report with a discussion of future avenues of research and an assessment of the work completed so far.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-618,
  author =	 {Shinwell, Mark R.},
  title = 	 {{The Fresh Approach: functional programming with names and
         	   binders}},
  year = 	 2005,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-618.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-618},
  number = 	 {UCAM-CL-TR-618}
}