Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

DOI10.4230/LIPIcs.CSL.2018.6OpenAlexW2888798587MaRDI QIDQ5079726

Kuen-Bang Hou (Favonia), Robert Harper, Carlo Angiuli

Publication date: 28 May 2022

Full work available at URL: https://dblp.uni-trier.de/db/conf/csl/csl2018.html#AngiuliF018

zbMATH Keywords

homotopy type theorycubical setscomputational type theorytwo-level type theory

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (9)

Cubical methods in homotopy type theory and univalent foundations ⋮ Finitary type theories with and without contexts ⋮ A formal logic for formal category theory ⋮ Two-level type theory and applications ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• HoTT
• cubicaltt
• GitHub
• cart-cube

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Innovations in computational type theory using Nuprl
• Homotopy type theory in Lean
• Homotopy theory of simplicial sheaves in completely decomposable topologies
• Towards a Formally Verified Proof Assistant
• Constructive mathematics and computer programming
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Varieties of Cubical Sets
• Computational higher-dimensional type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Intensional interpretations of functionals of finite type I

This page was built for publication: Cartesian cubical computational type theory: Constructive reasoning with paths and equalities