Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes

DOI10.1109/LICS.2013.27zbMath1367.68060OpenAlexW1984902166MaRDI QIDQ5271058

Rasmus Ejlers Møgelberg, Lars Birkedal

Publication date: 3 July 2017

Published in: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/lics.2013.27

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functor categories, comma categories (18A25)

Related Items (12)

Unnamed Item ⋮ Lewis meets Brouwer: constructive strict implication ⋮ A model of guarded recursion with clock synchronisation ⋮ A model of PCF in guarded type theory ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Guarded cubical type theory ⋮ Constructive Modalities with Provability Smack

This page was built for publication: Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes