Carlo Angiuli

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.

Drafts

A Cubical Language for Bishop Sets
J. Sterling, C. Angiuli, D. Gratzer
Draft, September 2021
[PDF]

Publications

Syntax and Models of Cartesian Cubical Type Theory
C. Angiuli, G. Brunerie, T. Coquand, K. Hou (Favonia), R. Harper, D. R. Licata
To appear, Mathematical Structures in Computer Science
[PDF] [Agda]

Normalization for Cubical Type Theory
J. Sterling, C. Angiuli
LICS 2021 (Symposium on Logic in Computer Science)
[PDF]

Internalizing Representation Independence with Univalence
C. Angiuli, E. Cavallo, A. Mörtberg, M. Zeuner
POPL 2021 (ACM SIGPLAN Symposium on Principles of Programming Languages)
[PDF] [Agda] [Short Video] [Long Video]

Computational Semantics of Cartesian Cubical Type Theory
C. Angiuli
Ph.D. dissertation @ CMU
Received School of Computer Science Distinguished Dissertation Award
[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]

Talks

(Conference talks are listed above with publications.)

What's the deal with HoTT?
Boston Computation Club
May 29, 2021 @ online

Internalizing Representation Independence with Univalence
Homotopy Type Theory Electronic Seminar Talks (HoTTEST), February 25, 2021
PLunch, April 30, 2021 @ CMU
CHoCoLA Seminar, June 3, 2021 @ ENS de Lyon
MURI grant meeting, October 15, 2021 @ CMU

Univalent Mathematics: Theory and Implementation
with Anders Mörtberg
International Congress on Mathematical Software
July 15, 2020 @ online due to COVID-19

From raw terms to recollement
Workshop on Homotopy Type Theory/Univalent Foundations
July 5, 2020 @ online due to COVID-19

The redtt proof assistant
MURI grant meeting
March 6, 2020 @ CMU

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

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