Technical reports
An executable meta-language for inductive definitions with binders
March 2010, 171 pages
This technical report is based on a dissertation submitted March 2010 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Queens’ College.
DOI: 10.48456/tr-772
Abstract
A testable prototype can be invaluable for identifying bugs during the early stages of language development. For such a system to be useful in practice it should be quick and simple to generate prototypes from the language specification.
This dissertation describes the design and development of a new programming language called alphaML, which extends traditional functional programming languages with specific features for producing correct, executable prototypes. The most important new features of alphaML are for the handling of names and binding structures in user-defined languages. To this end, alphaML uses the techniques of nominal sets (due to Pitts and Gabbay) to represent names explicitly and handle binding correctly up to alpha-renaming. The language also provides built-in support for constraint solving and non-deterministic search.
We begin by presenting a generalised notion of systems defined by a set of schematic inference rules. This is our model for the kind of languages that might be implemented using alphaML. We then present the syntax, type system and operational semantics of the alphaML language and proceed to define a sound and complete embedding of schematic inference rules. We turn to program equivalence and define a standard notion of operational equivalence between alphaML expressions and use this to prove correctness results about the representation of data terms involving binding and about schematic formulae and inductive definitions.
The fact that binding can be represented correctly in alphaML is interesting for technical reasons, because the language dispenses with the notion of globally distinct names present in most systems based on nominal methods. These results, along with the encoding of inference rules, constitute the main technical payload of the dissertation. However, our approach complicates the solving of constraints between terms. Therefore, we develop a novel algorithm for solving equality and freshness constraints between nominal terms which does not rely on standard devices such as swappings and suspended permutations. Finally, we discuss an implementation of alphaML, and conclude with a summary of the work and a discussion of possible future extensions.
Full text
PDF (1.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-772,
author = {Lakin, Matthew R.},
title = {{An executable meta-language for inductive definitions with
binders}},
year = 2010,
month = mar,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-772.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-772},
number = {UCAM-CL-TR-772}
}