Guarded cubical type theory

DOI10.1007/s10817-018-9471-7zbMath1477.03034arXiv1611.09263OpenAlexW2962873201MaRDI QIDQ2319985

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

Publication date: 21 August 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

homotopy type theoryguarded recursioncubical type theory

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Type theory (03B38)

Related Items (6)

Cubical methods in homotopy type theory and univalent foundations ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Temporal refinements for guarded recursive types ⋮ Modal dependent type theory and dependent right adjoints ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• Coq
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Sheaves in geometry and logic: a first introduction to topos theory
• The simplicial model of univalent foundations (after Voevodsky)
• Canonicity for cubical type theory
• Rings of sets
• A Formalized Proof of Strong Normalization for Guarded Recursive Types
• 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
• Coproducts of De Morgan algebras
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Extensional Constructs in Intensional Type Theory
• A type theory for productive coprogramming via guarded recursion
• Internal type theory
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
• Step-indexed kripke models over recursive worlds
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Applicative programming with effects
• A model of guarded recursion with clock synchronisation

This page was built for publication: Guarded cubical type theory