Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
From MaRDI portal
Publication:5079726
DOI10.4230/LIPICS.CSL.2018.6OpenAlexW2888798587MaRDI QIDQ5079726FDOQ5079726
Authors: 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
Recommendations
- Syntax and models of Cartesian cubical type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Type theories from Barendregt's cube for theorem provers
- Constructing inductive-inductive types in cubical type theory
- Canonicity for cubical type theory
- Expressing computational complexity in constructive type theory
- A Complete Proof Synthesis Method for the Cube of Type Systems
- scientific article; zbMATH DE number 6694181
- Proof theory of constructive systems: inductive types and univalence
- Automated Deduction – CADE-20
Cites Work
- Innovations in computational type theory using Nuprl
- Title not available (Why is that?)
- Homotopy theoretic models of identity types
- Homotopy type theory. Univalent foundations of mathematics
- Towards a formally verified proof assistant
- Intensional interpretations of functionals of finite type I
- Homotopy theory of simplicial sheaves in completely decomposable topologies
- Constructive mathematics and computer programming
- Computational higher-dimensional type theory
- Extending homotopy type theory with strict equality
- Title not available (Why is that?)
- Nominal presentation of cubical sets models of type theory
- Homotopy type theory in Lean
- Cubical type theory: a constructive interpretation of the univalence axiom
- Varieties of cubical sets
Cited In (13)
- Model structure on the universe of all types in interval type theory
- Transpension: the right adjoint to the Pi-type
- Two-level type theory and applications
- On the identity type as the type of computational paths
- A formal logic for formal category theory
- Naive cubical type theory
- Implementing Euclid's straightedge and compass constructions in type theory
- Cubical methods in homotopy type theory and univalent foundations
- Finitary type theories with and without contexts
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Syntax and models of Cartesian cubical type theory
Uses Software
This page was built for publication: Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5079726)
