The number of extremal components of a rigid measure. - Carlo Angiuli; Hari Bercovici (J. Comb. Theory A, 2011)

Automatically Splitting a Two-Stage Lambda Calculus. - Nicolas Feltman; Carlo Angiuli; Umut A. Acar; Kayvon Fatahalian (ESOP, 2016)

Computational Higher Type Theory I: Abstract Cubical Realizability. - Carlo Angiuli; Robert Harper 001; Todd Wilson (CoRR, 2016)

Computational Higher Type Theory II: Dependent Cubical Realizability. - Carlo Angiuli; Robert Harper 001 (CoRR, 2016)

Homotopical patch theory. - Carlo Angiuli; Edward Morehouse; Daniel R. Licata; Robert Harper 001 (J. Funct. Program., 2016)

Computational higher-dimensional type theory. - Carlo Angiuli; Robert Harper 001; Todd Wilson (POPL, 2017)

Computational Higher Type Theory III: Univalent Universes and Exact Equality. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CoRR, 2017)

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CSL, 2018)

The RedPRL Proof Assistant (Invited Paper). - Carlo Angiuli; Evan Cavallo; Kuen-Bang Hou (Favonia); Robert Harper 001; Jonathan Sterling (LFMTP@FSCD, 2018)

Cubical Syntax for Reflection-Free Extensional Equality. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (FSCD, 2019)

Normalization for Cubical Type Theory. - Jonathan Sterling; Carlo Angiuli (LICS, 2021)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

Internalizing representation independence with univalence. - Carlo Angiuli; Evan Cavallo; Anders Mörtberg; Max Zeuner (Proc. ACM Program. Lang., 2021)

Computational Semantics of Cartesian Cubical Type Theory. - Carlo Angiuli (2021)

Controlling unfolding in type theory. - Daniel Gratzer; Jonathan Sterling; Carlo Angiuli; Thierry Coquand; Lars Birkedal (CoRR, 2022)

A Cubical Language for Bishop Sets. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (Log. Methods Comput. Sci., 2022)

An Order-Theoretic Analysis of Universe Polymorphism. - Kuen-Bang Hou (Favonia); Carlo Angiuli; Reed Mullanix (Proc. ACM Program. Lang., 2023)

A dependently-typed calculus of event telicity and culminativity. - Pavel Kovalev; Carlo Angiuli (CoRR, 2025)