cangiuli at cs.cmu.edu
I am a postdoc in the Computer Science Department at Carnegie Mellon University, where I received a Ph.D. under Robert Harper. I previously studied at Indiana University Bloomington, where I received a B.S. in Mathematics and in Computer Science.
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]
Computational Semantics of Cartesian Cubical Type Theory
C. Angiuli
Ph.D. dissertation @ CMU
[PDF]
[Slides]
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]
(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
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
HelloResearch team leader
Research-oriented workshop for undergraduate women in CS
October 26-28, 2018 @ Indiana University
[Website]
9129 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
cangiuli
carloangiuli
https://orcid.org/0000-0002-9590-3303