On the principles of dependent type theory
On Cartesian cubical type theory:
Jonathan Sterling, Carlo Angiuli, Normalization for Cubical Type Theory, 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021. (doi:10.1109/LICS52264.2021.9470719, arXiv:2101.11479)
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata, Syntax and models of Cartesian cubical type theory, Mathematical Structures in Computer Science, 31(4), 2021. (doi:10.1017/S0960129521000347)
Carlo Angiuli, Computational Semantics of Cartesian Cubical Type Theory, Ph.D. Thesis. (pdf)
On XTT:
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).
On universe polymorphism in dependent type theory via monads:
Last revised on November 14, 2025 at 16:00:30. See the history of this page for a list of all contributions to it.