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: https://pure.itu.dk/en/publications/denotational-s... |

## Abstract

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: | https://kar.kent.ac.uk/id/eprint/99279 (The current URI for this page, for reference purposes) |

- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV

- Depositors only (login required):