Canonicity for 2-dimensional type theory

DOI10.1145/2103656.2103697zbMATH Open1321.03049OpenAlexW4247853537MaRDI QIDQ2942884FDOQ2942884

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

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

zbMATH Keywords

category theorydependent typestype theoryhomotopy type theory

Mathematics Subject Classification ID

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

Cited In (8)

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

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)