Carlo Angiuli

cangiuli at cs.cmu.edu

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.

Drafts

Computational Semantics of Cartesian Cubical Type Theory
C. Angiuli
Draft, Ph.D. dissertation
[PDF]

Syntax and Models of Cartesian Cubical Type Theory
C. Angiuli, G. Brunerie, T. Coquand, K. Hou (Favonia), R. Harper, D. R. Licata
Draft, February 2019
[PDF + Agda]

Publications

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

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
C. Angiuli, K. Hou (Favonia), R. Harper
CSL 2018 (Computer Science Logic)
[PDF] [Slides] [Tech Report]

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

Meaning explanations at higher dimension
C. Angiuli, R. Harper
Indagationes Mathematicae, 29 (1), 2018
Special issue "L.E.J. Brouwer, fifty years later"
[PDF]

Computational Higher-Dimensional Type Theory
C. Angiuli, R. Harper, T. Wilson
POPL 2017 (ACM SIGPLAN Symposium on Principles of Programming Languages)
[PDF] [Slides] [Tech Report]

Homotopical Patch Theory
C. Angiuli, E. Morehouse, D. R. Licata, R. Harper
Journal of Functional Programming, 26, 2016
Special issue dedicated to ICFP 2014
[PDF]

Automatically Splitting a Two-Stage Lambda Calculus
N. Feltman, C. Angiuli, U. A. Acar, K. Fatahalian
ESOP 2016 (European Symposium on Programming)
[PDF]

Homotopical Patch Theory
C. Angiuli, E. Morehouse, D. R. Licata, R. Harper
ICFP 2014 (ACM SIGPLAN International Conference on Functional Programming)
(I suggest the JFP version above.)
[Expanded Version] [Slides] [Video]

The number of extremal components of a rigid measure
C. Angiuli, H. Bercovici
Journal of Combinatorial Theory, Series A, 118 (7), 2011
[PDF] [arXiv]

Talks

(Conference talks are listed above with publications.)

Cartesian cubical type theory: computing with univalence
PL Wonks Seminar
November 2, 2018 @ Indiana University

Dependent types: from intuitionism to homotopy theory
Logic Seminar
October 31, 2018 @ Indiana University

Two Notions of Equality and Variable
Bob Harper Festschrift
September 22, 2018 @ CMU

Cartesian cubical type theory
Midwest HoTT Seminar
May 26, 2018 @ University of Western Ontario

Computational semantics of Cartesian cubical type theory
MURI grant meeting
March 23, 2018 @ CMU

Computational semantics of Cartesian cubical type theory
Homotopy Type Theory Electronic Seminar Talks (HoTTEST)
March 15, 2018

Computational Cubical Type Theory
CSD Open House
March 5, 2018 @ CMU

Computational (Higher) Type Theory
with Robert Harper
POPL 2018 tutorial
January 8, 2018

Cubical Programs + Cubical Type Systems
MURI grant meeting
March 25, 2017 @ CMU

Computational Higher-Dimensional Type Theory
PLunch
December 9, 2016 @ CMU

Computational Higher Type Theory
with Robert Harper
MURI grant meeting
March 19, 2016 @ CMU

Programming with Cubical Type Theory
CMU Principles of Programming group retreat
October 30, 2015

Programming Applications of HoTT
MURI grant meeting
March 27, 2015 @ CMU

Software

redtt developer
Proof assistant for Cartesian cubical type theory
[GitHub]

yacctt developer
Experimental fork of the cubicaltt type checker (use redtt instead!)
[GitHub]

RedPRL developer
Proof assistant for Cartesian cubical computational type theory
[Website]

Courses

Instructor, Principles of Functional Programming (15-150)
Summer I 2014 @ CMU

TA, Type Systems for Programming Languages (15-814) with Karl Crary
Fall 2013 @ CMU

TA, Constructive Logic (15-317) with Karl Crary
Fall 2012 @ CMU

Service

HelloResearch team leader
Research-oriented workshop for undergraduate women in CS
October 26-28, 2018 @ Indiana University
[Website]

9005 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213