A type theory for productive coprogramming via guarded recursion

DOI10.1145/2603088.2603132MaRDI QIDQ4635656zbMATH OpenOpenAlexFDO

Authors 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

categorical semanticsdependent typesdenotational semanticscorecursionguarded recursion

Mathematics Subject Classification ID

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)

Recommendations

• Denotational semantics for guarded dependent type theory
• Guarded dependent type theory with coinductive types
• Productive coprogramming with guarded recursion
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Programming and reasoning with guarded recursion for coinductive types

Cited in

(18)

• Temporal refinements for guarded recursive types
• Productive coprogramming with guarded recursion
• Coinduction in Flow: The Later Modality in Fibrations
• Denotational semantics of recursive types in synthetic guarded domain theory
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Modal dependent type theory and dependent right adjoints
• Lewis meets Brouwer: constructive strict implication
• A model of PCF in guarded type theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Programming and reasoning with guarded recursion for coinductive types
• Guarded dependent type theory with coinductive types
• Multimodal dependent type theory
• Denotational semantics for guarded dependent type theory
• scientific article; zbMATH DE number 7559298 (Why is no real title available?)
• Denotational semantics of recursive types in synthetic guarded domain theory
• Guarded cubical type theory
• A model of guarded recursion with clock synchronisation
• A model of guarded recursion via generalised equilogical spaces

Describes a project that uses

Uses Software

• Coq
• Agda

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)