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. I previously studied at Indiana University Bloomington, where I received a B.S. in Mathematics and in Computer Science.

Drafts

Syntax and Models of Cartesian Cubical Type Theory
C. Angiuli, G. Brunerie, T. Coquand, K. Hou (Favonia), R. Harper, D. R. Licata
Draft, March 2021
[PDF] [Agda]

A Cubical Language for Bishop Sets
J. Sterling, C. Angiuli, D. Gratzer
Draft, February 2020
[PDF]

Publications

Normalization for Cubical Type Theory
J. Sterling, C. Angiuli
To appear, 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.)

Internalizing Representation Independence with Univalence
Homotopy Type Theory Electronic Seminar Talks (HoTTEST), February 25, 2021
PLunch, April 30, 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 @ 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

Software

redtt developer
Proof assistant for Cartesian cubical type theory
[GitHub]

yacctt developer
Experimental fork of the cubicaltt type checker (use redtt instead!)
[GitHub]

RedPRL developer
Proof assistant for Cartesian cubical computational type theory
[Website]

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

Service

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

9129 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