Computational Higher Type Theory IV: Inductive Types. - Evan Cavallo; Robert Harper 001 (CoRR, 2018)

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

Parametric Cubical Type Theory. - Evan Cavallo; Robert Harper 001 (CoRR, 2019)

Stable factorization from a fibred algebraic weak factorization system. - Evan Cavallo (CoRR, 2019)

Higher inductive types in cubical computational type theory. - Evan Cavallo; Robert Harper 001 (Proc. ACM Program. Lang., 2019)

Unifying Cubical Models of Univalent Type Theory. - Evan Cavallo; Anders Mörtberg; Andrew W. Swan (CSL, 2020)

Internal Parametricity for Cubical Type Theory. - Evan Cavallo; Robert Harper 001 (Log. Methods Comput. Sci., 2021)

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

Higher Inductive Types and Internal Parametricity for Cubical Type Theory. - Evan Cavallo (2021)

Modalities and Parametric Adjoints. - Daniel Gratzer; Evan Cavallo; G. A. Kavvos; Adrien Guatto; Lars Birkedal (ACM Trans. Comput. Log., 2022)

Automating Boundary Filling in Cubical Agda. - Maximilian Doré; Evan Cavallo; Anders Mörtberg (FSCD, 2024)

The equivariant model structure on cartesian cubical sets. - Steve Awodey; Evan Cavallo; Thierry Coquand; Emily Riehl; Christian Sattler (CoRR, 2024)