Carlo Angiuli
9005 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
cangiuli at 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.
Preprints (selected)

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)
Publications

J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Syntax for ReflectionFree Extensional Equality.
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.
(Received Best Paper Award by Junior Researchers;
PDF,
Extended Version)

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,
Tech Report)

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,
Tech Report)

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)
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.
Software
 I contribute to RedPRL, a proof assistant based on computational cubical
type theory.
(GitHub,
website)
Other coordinates