Computational higher-dimensional type theory

DOI10.1145/3009837.3009861MaRDI QIDQ5370902zbMATH OpenOpenAlexFDO

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

(27)

• 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
• Groupoidal realizability for intensional type theory
• Analyticity and syntheticity in type theory revisited
• Constructing higher inductive types as groupoid quotients
• scientific article; zbMATH DE number 7215286 (Why is no real title available?)
• The construction of set-truncated higher inductive types
• Search algorithms in type theory
• An electrical engineering perspective on naturality in computational physics
• A normalizing computation rule for propositional extensionality in higher-order minimal logic
• Higher Structures in Homotopy Type Theory
• Higher types, finite domains and resource-bounded Turing machines
• scientific article; zbMATH DE number 2110617 (Why is no real title available?)
• Varieties of cubical sets
• scientific article; zbMATH DE number 1497732 (Why is no real title available?)
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Computations on types
• 2-Dimensional Directed Type Theory
• Syntax and models of Cartesian cubical type theory
• An introduction to univalent foundations for mathematicians
• The RedPRL proof assistant (invited paper)

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)