Canonicity for 2-dimensional type theory

DOI10.1145/2103656.2103697zbMath1321.03049OpenAlexW4247853537MaRDI QIDQ2942884

Robert Harper, Daniel R. Licata

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 theorytype theorydependent typeshomotopy type theory

Mathematics Subject Classification ID

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

Related Items

Homotopical patch theory ⋮ Meaning explanations at higher dimension ⋮ Bicategorical type theory: semantics and syntax

Uses Software

• Nuprl