This paper describes work in progress on the design of an ML-style metalanguage Fresh ML for programming with recursively defined functions on user-defined, concrete data types whose constructors may involve variable binding. Up to operational equivalence, values of such Fresh ML data types can faithfully encode terms modulo α-conversion for a wide range of object languages in a straightforward fashion. The design of Fresh ML is ‘semantically driven’, in that it arises from the model of variable binding in set theory with atoms given by the authors in [7]. The language has a type constructor for abstractions over names (= atoms) and facilities for declaring locally fresh names. Moreover, recursive definitions can use a form of pattern-matching on bound names in abstractions. The crucial point is that the Fresh ML type system ensures that these features can only be used in well-typed programs in ways that are insensitive to renaming of bound names.
CITATION STYLE
Pitts, A. M., & Gabbay, M. J. (2000). A metalanguage for programming with bound names modulo renaming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1837, pp. 230–255). Springer Verlag. https://doi.org/10.1007/10722010_15
Mendeley helps you to discover research relevant for your work.