## 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]