A type theory for productive coprogramming via guarded recursion
DOI10.1145/2603088.2603132zbMATH Open1394.68066OpenAlexW2165952355MaRDI QIDQ4635656FDOQ4635656
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
Categorical logic, topoi (03G30) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Foundations, relations to logic and deductive systems (18A15)
Cited In (16)
- Guarded Dependent Type Theory with Coinductive Types
- Denotational semantics of recursive types in synthetic guarded domain theory
- Temporal refinements for guarded recursive types
- Guarded cubical type theory
- Coinduction in Flow: The Later Modality in Fibrations
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Title not available (Why is that?)
- A model of guarded recursion with clock synchronisation
- A model of PCF in guarded type theory
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- Lewis meets Brouwer: constructive strict implication
- Denotational semantics for guarded dependent type theory
- Title not available (Why is that?)
- Modal dependent type theory and dependent right adjoints
- A model of guarded recursion via generalised equilogical spaces
- Denotational semantics of recursive types in synthetic guarded domain theory
Uses Software
This page was built for publication: A type theory for productive coprogramming via guarded recursion
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635656)
