A type theory for productive coprogramming via guarded recursion

DOI10.1145/2603088.2603132zbMath1394.68066OpenAlexW2165952355MaRDI QIDQ4635656

Rasmus Ejlers Møgelberg

Publication date: 23 April 2018

Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2603088.2603132

zbMATH Keywords

denotational semanticsdependent typescategorical semanticscorecursionguarded recursion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Foundations, relations to logic and deductive systems (18A15)

Related Items (14)

Lewis meets Brouwer: constructive strict implication ⋮ A model of guarded recursion via generalised equilogical spaces ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ 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 ⋮ Denotational semantics for guarded dependent type theory ⋮ Temporal refinements for guarded recursive types ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Modal dependent type theory and dependent right adjoints ⋮ Guarded cubical type theory ⋮ Unnamed Item

Uses Software

• Coq
• Agda

This page was built for publication: A type theory for productive coprogramming via guarded recursion