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.

**cangiuli at cs.cmu.edu**

**A Cubical Language for Bishop Sets**

J. Sterling, C. Angiuli, D. Gratzer

Draft, September 2021

[PDF]

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

*(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

**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*

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*

School of Computer Science

Carnegie Mellon University

5000 Forbes Ave

Pittsburgh, PA 15213