The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion

MaRDI QIDQ5144643zbMATH OpenFDO

Authors Patrick Bahr, Hans Bugge Grathwohl, Rasmus Ejlers Møgelberg

Publication date 19 January 2021

Full work available at URL http://dl.acm.org/citation.cfm?id=3330032

Mathematics Subject Classification ID

Type theory (03B38) Temporal logic (03B44)

Recommendations

• A model of guarded recursion with clock synchronisation
• Guarded dependent type theory with coinductive types
• Denotational semantics for guarded dependent type theory
• Guarded computational type theory
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

Cited in

(28)

• Temporal refinements for guarded recursive types
• A formalized proof of strong normalization for guarded recursive types
• Guarded dependent type theory with coinductive types
• Guarded recursive datatype constructors
• Programming and reasoning with guarded recursion for coinductive types
• scientific article; zbMATH DE number 1189292 (Why is no real title available?)
• Denotational semantics of recursive types in synthetic guarded domain theory
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• Guarded recursion in Agda via sized types
• Denotational semantics for guarded dependent type theory
• Guarded computational type theory
• Multimodal dependent type theory
• Modal dependent type theory and dependent right adjoints
• Productive coprogramming with guarded recursion
• Intensional type theory with guarded recursive types qua fixed points on universes
• Guarded cubical type theory: path equality for guarded recursion
• A model of guarded recursion with clock synchronisation
• A model of PCF in guarded type theory
• When programs have to watch paint dry
• Modal FRP for all: Functional reactive programming without space leaks in Haskell
• Streams of approximations, equivalence of recursive effectful programs
• A stratified approach to Löb induction
• Transpension: the right adjoint to the Pi-type
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Classifying topoi in synthetic guarded domain theory
• What monads can and cannot do with a bit of extra time
• What monads can and cannot do with a few extra pages
• A sound and complete substitution algorithm for multimode type theory

This page was built for publication: The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5144643)