Guarded Cubical Type Theory: Path Equality for Guarded Recursion

DOI10.4230/LIPICS.CSL.2016.23zbMath1370.68052arXiv1606.05223OpenAlexW2963775463MaRDI QIDQ5278409

Ranald Clouston, Bas Spitters, Hans Bugge Grathwohl, Andrea Vezzosi, Aleš Bizjak, Lars Birkedal

Publication date: 19 July 2017

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

zbMATH Keywords

denotational semanticshomotopy type theorydependent type theoryguarded recursioncubical type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Topological categories, foundations of homotopy theory (55U40)

Related Items (6)

Unnamed Item ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ Denotational semantics for guarded dependent type theory ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Guarded cubical type theory ⋮ Unnamed Item

Uses Software

• Unnamed Item

This page was built for publication: Guarded Cubical Type Theory: Path Equality for Guarded Recursion