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

• C. Angiuli, G. Brunerie, T. Coquand, K. Hou (Favonia), R. Harper, and D. R. Licata. Cartesian Cubical Type Theory. December 2017. (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