nLab Carlo Angiuli

• personal page.

• GoogleScholar page

Publications

On the principles of dependent type theory

• Carlo Angiuli, Daniel Gratzer, Principles of Dependent Type Theory (pdf)

On computational higher type theory:

• Computational Higher Type Theory I: Abstract Cubical Realizability, Carlo Angiuli, Robert Harper, Todd Wilson, arxiv, 2016
• Computational Higher Type Theory II: Dependent Cubical Realizability, Carlo Angiuli, Robert Harper, arxiv, 2016
• Computational Higher Type Theory III: Univalent Universes and Exact Equality, Carlo Angiuli, Kuen-Bang Hou, Robert Harper, arxiv, 2017

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:

• Favonia, Carlo Angiuli, Reed Mullanix, An Order-Theoretic Analysis of Universe Polymorphism, Proceedings of the ACM on Programming Languages 7 57 (2023) 1659–1685 [doi:10.1145/3571250]

category: people