School of Computing

Nov 6
15:00 - 16:00
PLAS: Marco Paviotti
PLAS Group Seminar
Denotational semantics in Synthetic Guarded Domain Theory

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.

Location

SW101,
Cornwallis South West,
University of Kent,
Canterbury,
Kent,
CT2 7NF
United Kingdom
Map

Details

Contact: O.Chitil
E: oc@kent.ac.uk
School of Computing

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 14/08/2015