Skip to main content
Kent Academic Repository

Denotational semantics in Synthetic Guarded Domain Theory

Paviotti, Marco (2016) Denotational semantics in Synthetic Guarded Domain Theory. ITU-DS, 126 . IT-Universitetet i København, Copenhagen, Denmark, 143 pp. ISBN 978-87-7949-345-2. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:99279)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL:


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.

Step-indexing is a more general technique that has been used to break circularity of definitions. The idea is to tweak the definition by adding a well-founded structure that gives a handle for recursion. Guarded dependent Type Theory (gDTT) is a type theory which implements step-indexing via a unary modality used to guard recursive definitions. Every circular definition is well-defined as long as the recursive variable is guarded.

In this thesis we show that gDTT 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. Furthermore, our interpretation is synthetic: types are interpreted as types in the type theory and programs as type-theoretical terms. Moreover, working directly in gDTT has advantages compared with existing set-theoretic models.

Finally, this work builds the foundations for doing denotational semantics of languages with much more challenging features, for example, of general references for which denotational techniques were previously beyond reach.

Item Type: Book
Uncontrolled keywords: Category Theory, Type Theory, Recursion, Fixed-Points, Guarded Recursion, Domain Theory
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Marco Paviotti
Date Deposited: 21 Dec 2022 20:38 UTC
Last Modified: 06 Jan 2023 17:24 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.