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.
I study the mathematics of programming
languages and their type systems. My current research interests focus on
computational aspects of homotopy type
theory and related systems. In particular, I develop univalent type theories
with computational content, and study their programming applications. But I find
anything with logical relations or dependent types interesting.
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, K. Hou (Favonia), and R. Harper.
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.
Computer Science Logic (CSL), 2018.
(PDF, Slides)

C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling.
The RedPRL Proof Assistant. (Invited Paper)
International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP), 2018.
(PDF, Proceedings)

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.
(Superseded 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

J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Syntax for ReflectionFree Extensional Equality.
February 2019.
(PDF)

C. Angiuli, G. Brunerie, T. Coquand, K. Hou (Favonia), R. Harper, and D. R. Licata.
Syntax and Models of Cartesian Cubical Type Theory.
February 2019.
(GitHub)

C. Angiuli, K. 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.
(Superseded by Part III; arXiv)

C. Angiuli, R. Harper, and T. Wilson.
Computational Higher Type Theory I: Abstract Cubical Realizability.
April 2016.
(Superseded by Part II; arXiv)
Software
 I contribute to RedPRL, a proof assistant based on computational cubical
type theory.
(GitHub,
website)
Other coordinates