The clocks they are adjunctions. Denotational semantics for clocked type theory

DOI10.4230/LIPICS.FSCD.2018.23MaRDI QIDQ4993353zbMATH OpenFDO

Authors Bassel Mannaa, Rasmus Ejlers Møgelberg

Publication date 15 June 2021

Full work available at URL https://arxiv.org/abs/1804.06687

zbMATH Keywords

clocked type theorycoinductiondependent adjunctionguarded type theorypresheaf model

Mathematics Subject Classification ID

Type theory (03B38) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 7288622
• Denotational semantics for guarded dependent type theory
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• Guarded dependent type theory with coinductive types
• Guarded computational type theory

Cites work

• A dependent type theory with abstractable names
• A model of countable nondeterminism in guarded type theory
• A presheaf model of parametric type theory
• Applicative programming with effects
• Cubical type theory: a constructive interpretation of the univalence axiom
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Homotopy type theory. Univalent foundations of mathematics
• Intensional type theory with guarded recursive types qua fixed points on universes
• Internal type theory
• Productive coprogramming with guarded recursion

Cited in

(7)

• Guarded recursion in Agda via sized types
• Denotational semantics for guarded dependent type theory
• Multimodal dependent type theory
• Modal dependent type theory and dependent right adjoints
• When programs have to watch paint dry
• Modal FRP for all: Functional reactive programming without space leaks in Haskell
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: The clocks they are adjunctions. Denotational semantics for clocked type theory

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