Projects per year
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 programming languages with advanced features including general references, recursive types, countable nondeterminism 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 using 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 computationally 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 intensional 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.
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 using 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 computationally 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 intensional 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.
Original language  English 

Title of host publication  LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science 
Number of pages  10 
Publisher  Association for Computing Machinery 
Publication date  2016 
Pages  317326 
ISBN (Print)  9781450343916 
DOIs  
Publication status  Published  2016 
Keywords
 Guarded Recursion
 Denotational Semantics
 Type Theory
 Recursive Types
 Computational Adequacy
Fingerprint
Dive into the research topics of 'Denotational semantics of recursive types in synthetic guarded domain theory'. Together they form a unique fingerprint.Projects
 1 Finished

Guarded recursive types in the foundations of programming
Møgelberg, R. E. (PI), Mannaa, B. (CoI) & Bahr, P. (CoI)
Independent Research Fund Denmark
01/07/2015 → 31/01/2019
Project: Research