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; before that, I studied Mathematics and Computer Science at Indiana University Bloomington.

I study programming languages through the lens of type theory, a logical framework for computer programs and mathematical proofs. My main research interests are in dependent types and specifically homotopy type theory, an interdisciplinary area at the nexus between type theory and (mathematical) abstract homotopy theory.

I look for fundamental ideas in type theory that can enable practical advances in its expressivity and ease of use. Currently, I'm pursuing ideas from homotopy type theory that address pain points of formal verification in proof assistants; for example, the univalence axiom can be used to deduce representation independence theorems in Cubical Agda [POPL '21].

New! I'm making a series of videos on category theory aimed at people who have some previous exposure to the subject but who don't feel they "get it." These videos will cover introductory-level topics from a more sophisticated, unifying perspective than is usually presented to beginners.

Preprints

Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, L. Birkedal
Preprint, October 2022
[PDF]

Publications

An Order-Theoretic Analysis of Universe Polymorphism
K. Hou (Favonia), C. Angiuli, R. Mullanix
POPL 2023 (ACM SIGPLAN Symposium on Principles of Programming Languages)
[PDF] [OCaml] [Agda]

A Cubical Language for Bishop Sets
J. Sterling, C. Angiuli, D. Gratzer
Logical Methods in Computer Science, 18 (1), 2022
[PDF]

Syntax and models of Cartesian cubical type theory
C. Angiuli, G. Brunerie, T. Coquand, R. Harper, K. Hou (Favonia), D. R. Licata
Mathematical Structures in Computer Science, 31 (4), 2021
Special issue on Homotopy Type Theory and Univalent Foundations
[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.)

Controlled definitional opacity in proof assistants
MURI grant meeting
June 30, 2022 @ CMU

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
POPV Seminar, November 2, 2022 @ Boston University

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

Service

Co-organizer, HoTTEST Summer School 2022
Online two-month summer school for homotopy type theory
[Website]

Co-organizer, HoTTEST seminar series, Fall 2021–
(Homotopy Type Theory Electronic Seminar Talks)
[Website]

PC member, TYPES 2022
(International Conference on Types for Proofs and Programs)
[Website]

PC member, HoTT/UF 2021 and 2022
(Workshop on Homotopy Type Theory/Univalent Foundations)
[2022 Website] [2021 Website]

Co-chair, Univalent Mathematics: Theory and Implementation session at ICMS 2020
(International Congress on Mathematical Software)
[Website] [ICMS Website]

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

Chair of local organizing committee, Bob Harper Festschrift
September 22, 2018 @ CMU
[Website]

Software

red* proof assistant
Co-developer of several experimental proof assistants for Cartesian cubical type theory
[Website] [cooltt GitHub] [redtt GitHub] [RedPRL GitHub]

yacctt
Co-developer of an experimental fork of the cubicaltt type checker (use redtt instead!)
[GitHub]

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

9213 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