scientific article; zbMATH DE number 7359419

DOI10.4230/LIPIcs.FSCD.2018.23zbMath1462.68023arXiv1804.06687MaRDI QIDQ4993353

Bassel Mannaa, Rasmus Ejlers Møgelberg

Publication date: 15 June 2021

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

coinductionpresheaf modelclocked type theorydependent adjunctionguarded type theory

Mathematics Subject Classification ID

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

Related Items (6)

When programs have to watch paint dry ⋮ Modal FRP for all: Functional reactive programming without space leaks in Haskell ⋮ Denotational semantics for guarded dependent type theory ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Unnamed Item

Uses Software

• cubicaltt

Cites Work

• A dependent type theory with abstractable names
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• A Model of Countable Nondeterminism in Guarded Type Theory
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Applicative programming with effects
• A presheaf model of parametric type theory

This page was built for publication: