Computational higher-dimensional type theory
DOI10.1145/3009837.3009861zbMATH Open1380.68112OpenAlexW2562854264MaRDI QIDQ5370902FDOQ5370902
Authors: Robert Harper, Todd Wilson, Carlo Angiuli 
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
Recommendations
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 (23)
- Canonicity for cubical type theory
- Canonicity for 2-dimensional type theory
- Foundations of mathematics in polymorphic type theory
- Interpreting higher computations as types with totality
- Towards a cubical type theory without an interval
- Constructing higher inductive types as groupoid quotients
- 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?)
- Varieties of cubical sets
- 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
- 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)
