Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
From MaRDI portal
Publication:5271058
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
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
