Computational higher-dimensional type theory

DOI10.1145/3009837.3009861MaRDI QIDQ5370902zbMATHOpenAlexFDO

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

zbMATH Keywords

logical relationshomotopy type theory

Mathematics Subject Classification ID

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)

Recommendations

• Canonicity for 2-dimensional type theory
• Meaning explanations at higher dimension
• On higher inductive types in cubical type theory
• Canonicity for cubical type theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory

Cited in

(23)

• An introduction to univalent foundations for mathematicians
• scientific article; zbMATH DE number 7215286 (Why is no real title available?)
• An electrical engineering perspective on naturality in computational physics
• Higher types, finite domains and resource-bounded Turing machines
• scientific article; zbMATH DE number 2110617 (Why is no real title available?)
• Computations on types
• Constructing higher inductive types as groupoid quotients
• Foundations of mathematics in polymorphic type theory
• Varieties of cubical sets
• Towards a cubical type theory without an interval
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• Higher Structures in Homotopy Type Theory
• Canonicity for cubical type theory
• scientific article; zbMATH DE number 1497732 (Why is no real title available?)
• 2-Dimensional Directed Type Theory
• Canonicity for 2-dimensional type theory
• Syntax and models of Cartesian cubical type theory
• The construction of set-truncated higher inductive types
• Interpreting higher computations as types with totality
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Search algorithms in type theory

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)