Computational higher-dimensional type theory
From MaRDI portal
Publication:5370902
DOI10.1145/3009837.3009861zbMath1380.68112OpenAlexW2562854264MaRDI QIDQ5370902
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
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Varieties of Cubical Sets, The construction of set-truncated higher inductive types, Unnamed Item, Homotopy type theory in Lean, Meaning explanations at higher dimension, Higher Structures in Homotopy Type Theory, An introduction to univalent foundations for mathematicians, Unnamed Item, Unnamed Item, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Canonicity for cubical type theory, Towards a Cubical Type Theory without an Interval, Syntax and models of Cartesian cubical type theory
