Canonicity for 2-dimensional type theory

DOI10.1145/2103656.2103697MaRDI QIDQ2942884zbMATH OpenOpenAlexFDO

Authors Daniel R. Licata, Robert Harper

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.208.1826

zbMATH Keywords

category theorydependent typeshomotopy type theorytype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Recommendations

• Computational higher-dimensional type theory
• 2-Dimensional Directed Type Theory
• Canonicity for cubical type theory
• Two-dimensional models of type theory
• Canonicity and homotopy canonicity for cubical type theory

Cited in

(9)

• Meaning explanations at higher dimension
• Two-dimensional models of type theory
• On equivalence and canonical forms in the LF type theory
• Computational higher-dimensional type theory
• Homotopical patch theory
• 2-Dimensional Directed Type Theory
• Bicategorical type theory: semantics and syntax
• Semantics for two-dimensional type theory
• A normalizing computation rule for propositional extensionality in higher-order minimal logic

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Canonicity for 2-dimensional type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942884)