Skip to main content

Denotational semantics of recursive types in synthetic guarded domain theory

Paviotti, Marco, Møgelberg, Rasmus (2016) Denotational semantics of recursive types in synthetic guarded domain theory. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. . ISBN 978-1-4503-4391-6. (doi:10.1145/2933575.2934516) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided)

PDF - Author's Accepted Manuscript
Restricted to Repository staff only
Contact us about this Publication Download (271kB)
[img]
Official URL
http://dx.doi.org/10.1145/2933575.2934516

Abstract

Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for reasoning operationally about pro- gramming languages with advanced features including general ref- erences, recursive types, countable non-determinism and concurrency. Guarded recursion also offers a way of adding recursion to type theory while maintaining logical consistency. In previous work we initiated a programme of denotational semantics in type theory us- ing guarded recursion, by constructing a computationally adequate model of the language PCF (simply typed lambda calculus with fixed points). This model was intensional in that it could distinguish between computations computing the same result using a different number of fixed point unfoldings. In this work we show how also programming languages with recursive types can be given denotational semantics in type theory with guarded recursion. More precisely, we give a computation- ally adequate denotational semantics to the language FPC (simply typed lambda calculus extended with recursive types), modelling recursive types using guarded recursive types. The model is inten- sional in the same way as was the case in previous work, but we show how to recover extensionality using a logical relation. All constructions and reasoning in this paper, including proofs of theorems such as soundness and adequacy, are by (informal) reasoning in type theory, often using guarded recursion.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2933575.2934516
Uncontrolled keywords: Recursive Types, Type Theory, Denotational semantics, Category Theory, Domain Theory
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Marco Paviotti
Date Deposited: 05 Dec 2017 15:17 UTC
Last Modified: 29 May 2019 19:59 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/65016 (The current URI for this page, for reference purposes)
Paviotti, Marco: https://orcid.org/0000-0002-1513-0807
  • Depositors only (login required):

Downloads

Downloads per month over past year