Denotational semantics for guarded dependent type theory

DOI10.1017/S0960129520000080zbMath1495.68127arXiv1802.03744OpenAlexW3022922601MaRDI QIDQ5139284

Rasmus Ejlers Møgelberg, Aleš Bizjak

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

denotational semanticstype theoryguarded recursioncoinductive types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Type theory (03B38)

Related Items (4)

Unnamed Item ⋮ Temporal refinements for guarded recursive types ⋮ Modal dependent type theory and dependent right adjoints ⋮ Unnamed Item

Uses Software

• Coq
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Guarded Dependent Type Theory with Coinductive Types
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A very modal model of a modern, major, general type system
• The Discrete Objects in the Effective Topos
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A type theory for productive coprogramming via guarded recursion
• Denotational semantics of recursive types in synthetic guarded domain theory
• Internal type theory
• Guarded Computational Type Theory
• A Model of Countable Nondeterminism in Guarded Type Theory
• Wellfounded recursion with copatterns
• Productive coprogramming with guarded recursion
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects
• A model of guarded recursion with clock synchronisation

This page was built for publication: Denotational semantics for guarded dependent type theory