Computational higher-dimensional type theory
DOI10.1145/3009837.3009861zbMATH Open1380.68112OpenAlexW2562854264MaRDI QIDQ5370902FDOQ5370902
Carlo Angiuli, Robert Harper, Todd Wilson
Publication date: 20 October 2017
Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/3009837.3009861
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical logic, topoi (03G30) Semantics in the theory of computing (68Q55)
Cited In (22)
- Canonicity for cubical type theory
- Foundations of mathematics in polymorphic type theory
- Title not available (Why is that?)
- Interpreting higher computations as types with totality
- Varieties of Cubical Sets
- Title not available (Why is that?)
- The construction of set-truncated higher inductive types
- An electrical engineering perspective on naturality in computational physics
- Search algorithms in type theory
- Higher Structures in Homotopy Type Theory
- Higher types, finite domains and resource-bounded Turing machines
- Title not available (Why is that?)
- Title not available (Why is that?)
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Title not available (Why is that?)
- Computations on types
- Towards a Cubical Type Theory without an Interval
- 2-Dimensional Directed Type Theory
- Syntax and models of Cartesian cubical type theory
- An introduction to univalent foundations for mathematicians
This page was built for publication: Computational higher-dimensional type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370902)
