Carlo Angiuli
9005 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
ca...@cs.cmu.edu
http://www.carloangiuli.com/blog
I am a Ph.D. student in the Computer Science Department at Carnegie Mellon University, advised by Robert Harper. I previously studied at Indiana University Bloomington, where I received
a B.S. in Mathematics and in Computer Science.
Research
I am interested in programming language
theory, applied logic, and the parts of mathematics not involving
numbers.
I am currently working on programming applications of homotopy type theory, an extension
of MartinLöf type theory to a highercategorical setting.
Teaching
 Summer I 2014 — Instructor for Principles of Functional Programming
(15150).
 Fall 2013 — TA for Type Systems for Programming Languages
(15814) with
Karl Crary.
 Fall 2012 — TA for Constructive Logic
(15317) with
Karl Crary.
Publications

C. Angiuli and R. Harper.
Meaning explanations at higher dimension.
Indagationes Mathematicae (special issue
L.E.J. Brouwer, fifty years later), 2017.
(PDF)

C. Angiuli, R. Harper, and T. Wilson.
Computational HigherDimensional Type Theory.
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017.
(PDF,
Slides)

C. Angiuli, E. Morehouse, D. R. Licata, and R. Harper.
Homotopical Patch Theory.
Journal of Functional Programming (JFP), 2016.
(PDF)

N. Feltman, C. Angiuli, U. A. Acar, and K. Fatahalian.
Automatically Splitting a TwoStage Lambda Calculus.
European Symposium on Programming (ESOP), 2016.
(PDF)

C. Angiuli, E. Morehouse, D. R. Licata, and R. Harper.
Homotopical Patch Theory.
ACM SIGPLAN International Conference on Functional Programming (ICFP), 2014.
(Superceded by JFP version above;
Expanded Version,
Slides,
Video)

Angiuli, C. and Bercovici, H. The number of extremal components of a rigid
measure. Journal of Combinatorial Theory, Series A, Volume 118, Issue
7, 19251938. October 2011.
(PDF,
arXiv)
Preprints

C. Angiuli, G. Brunerie, T. Coquand, K.B. Hou (Favonia), R. Harper, and D. R. Licata.
Cartesian Cubical Type Theory.
December 2017.
(GitHub)

C. Angiuli, K.B. Hou (Favonia), and R. Harper.
Computational Higher Type Theory III: Univalent Universes and Exact Equality.
December 2017.
(arXiv)

C. Angiuli and R. Harper.
Computational Higher Type Theory II: Dependent Cubical Realizability.
June 2016.
(arXiv)

C. Angiuli, R. Harper, and T. Wilson.
Computational Higher Type Theory I: Abstract Cubical Realizability.
April 2016.
(arXiv)
Other coordinates