Evan Cavallo

I'm a 6th-year Ph.D. student in computer science at Carnegie Mellon University, in the Principles of Programming group. I am advised by Robert Harper and study cubical type theories and their ilk.
Address mail to ecavallo, zip code cs.cmu.edu.

Publications

20.07 | Internalizing representation independence with univalence.
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, & Max Zeuner.
Principles of Programming Languages (POPL) 2021.
[Paper] [Cubical Agda]
20.01 | Internal parametricity for cubical type theory.
Evan Cavallo & Robert Harper.
Computer Science Logic (CSL) 2020.
[Paper] [Tech report]
20.01 | Unifying cubical models of univalent type theory.
Evan Cavallo, Anders Mörtberg, & Andrew W Swan.
Computer Science Logic (CSL) 2020.
[Paper] [Tech report: type theory] [Tech report: model structure] [Agda formalization]
19.01 | Higher inductive types in cubical computational type theory.
Evan Cavallo & Robert Harper.
Principles of Programming Languages (POPL) 2019.
[Paper] [Tech report]
18.07 | The RedPRL proof assistant.
Carlo Angiuli, Evan Cavallo, Favonia, Robert Harper, & Jonathan Sterling.
Logical Frameworks & Meta Languages: Theory & Practice (LFMTP) 2018. Invited paper.
[Paper]

Preprints, notes, &c.

21.01 | Modalities and parametric adjoints.
Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, & Lars Birkedal.
[Preprint]
20.05 | Internal parametricity for cubical type theory.
Evan Cavallo & Robert Harper.
Extended version of CSL 2020 paper, in preparation.
[arXiv]
19.10 | "Stable factorization from a fibred algebraic weak factorization system".
Evan Cavallo.
Unpublished note.
[arXiv]
15.12 | Synthetic cohomology in homotopy type theory.
Evan Cavallo.
Master's thesis in Mathematical Sciences @ Carnegie Mellon U.
[Thesis]

Code

ptt [Github]
An experimental implementation of a type-checker for a type theory with internal parametricity, using Gratzer, Sterling, and Birkedal's blott as a base.

Talks

20.01 | Internal parametricity for cubical type theory @ CSL 2020. [Slides]
20.01 | Unifying cubical models of univalent type theory @ CSL 2020. [Slides]
19.06 | Cubical indexed inductive types @ HoTT-UF 2019 (invited talk). [Slides]
19.06 | Internally parametric cubical type theory @ TYPES 2019. [Slides]
19.03 | Parametric cubical type theory @ HoTTEST. [Slides] [Video]
19.01 | Higher inductive types in cubical computational type theory @ POPL 2019. [Slides] [Video]
14.09 | The Mayer-Vietoris sequence and cubes @ Oxford HoTT Workshop. [Slides] [Note] [Video]

Teaching

16.Fa | TA for 15-317 Constructive Logic.
15.Fa | TA for 15-814 Types and Programming Languages.
15.Sp | TA for 15-312 Foundations of Programming Languages.
14.Fa | TA for 15-317 Constructive Logic.

Status

15-?? | Ph.D. student in Computer Science @ Carnegie Mellon U.
10-15 | Undergraduate & Honors Master's student in Mathematical Sciences @ Carnegie Mellon U.