Carlo Angiuli

I am an assistant professor of computer science in the Luddy School at Indiana University. I study programming languages and logic through the lens of type theory, a logical framework for computer programs and mathematical proofs; I like to look for fundamental ideas in type theory that can enable practical advances in its expressivity and ease of use. My main research interests are in dependent types, proof assistants, and homotopy type theory.


I'm lecturing at the School on Univalent Mathematics at the University of Minnesota in July 2024.

Daniel Gratzer and I are writing lecture notes on the modern design of dependent type theories. Feedback welcome!

I'm on the program committee for HOPE 2024.

I'm moving to Indiana University in August 2023!


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


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

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)

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"

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

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

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]


PL Wonks
Programming languages seminar at Indiana University

Videos on category theory
Introductory topics covered from a more sophisticated, unifying perspective than is usually presented to beginners

HoTTEST Summer School 2022
Online two-month summer school for homotopy type theory

Homotopy Type Theory Electronic Seminar Talks
Online research seminar with hour-long talks every other week

red* family of proof assistants
Several experimental proof assistants for Cartesian cubical type theory
[Website] [cooltt GitHub] [redtt GitHub] [RedPRL GitHub]


Modern Dependent Types (Topics in Applied Logic)
Spring 2024

Introduction to Computer Science – Honors
Fall 2023

Luddy Hall 3008
700 N Woodlawn Ave
Bloomington, IN 47408