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.

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]

Teaching

Programming Language Foundations
Spring 2025

Modern Dependent Types (Topics in Applied Logic)
Spring 2024
[Website]

Introduction to Computer Science – Honors
Fall 2023, Fall 2024