In functional programming, features such as recursion, recursive types and general references are central. To define semantics of this kind of languages one needs to come up with certain definitions which may be non-trivial to show well-defined. This is because they are circular. Domain theory has been used to solve this kind of problems for specific languages, unfortunately, this technique does not scale for more featureful languages, which prevented it from being widely used.
In this work we show that Synthetic Guarded Domain theory (SGDT) is a natural setting to give denotational semantics of typed functional programming languages with recursion and recursive types. We formulate operational semantics and denotational semantics and prove computational adequacy entirely inside the type theory of SGDT. Furthermore, our interpretation is synthetic: types are interpreted as types in the type theory and programs as type-theoretical terms. Moreover, working directly in SGDT has advantages compared with existing set-theoretic models.
Cornwallis South West,
University of Kent,