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
(15-150).
- Fall 2013 — TA for Type Systems for Programming Languages
(15-814) with
Karl Crary.
- Fall 2012 — TA for Constructive Logic
(15-317) 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 Meta-Languages: 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 Higher-Dimensional 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 Two-Stage 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, 1925-1938. October 2011.
(PDF,
arXiv)
Preprints
-
J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Syntax for Reflection-Free 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
