Denotational semantics for guarded dependent type theory

DOI10.1017/S0960129520000080zbMath1495.68127arXiv1802.03744MaRDI 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 semantics; type theory; guarded recursion; coinductive types

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q55: Semantics in the theory of computing

18F20: Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects)

03B38: Type theory

Uses Software

• Coq
• cubicaltt