Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
From MaRDI portal
Publication:5079726
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
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- Computational higher-dimensional type theory
- Constructive mathematics and computer programming
- Cubical type theory: a constructive interpretation of the univalence axiom
- Extending homotopy type theory with strict equality
- Homotopy theoretic models of identity types
- Homotopy theory of simplicial sheaves in completely decomposable topologies
- Homotopy type theory in Lean
- Homotopy type theory. Univalent foundations of mathematics
- Innovations in computational type theory using Nuprl
- Intensional interpretations of functionals of finite type I
- Nominal presentation of cubical sets models of type theory
- Towards a formally verified proof assistant
- Varieties of cubical sets
Cited in
(13)- Model structure on the universe of all types in interval type theory
- Two-level type theory and applications
- A formal logic for formal category theory
- Finitary type theories with and without contexts
- Naive cubical type theory
- Implementing Euclid's straightedge and compass constructions in type theory
- Transpension: the right adjoint to the Pi-type
- Cubical methods in homotopy type theory and univalent foundations
- Syntax and models of Cartesian cubical type theory
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- scientific article; zbMATH DE number 7559297 (Why is no real title available?)
- On the identity type as the type of computational paths
- scientific article; zbMATH DE number 7566056 (Why is no real title available?)
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)
