Evan Cavallo


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


Publications


20.01 | Internal parametricity for cubical type theory.
Evan Cavallo & Robert Harper.
To appear in Computer Science Logic (CSL) 2020.
[Paper] [Technical report]
20.01 | Unifying cubical models of univalent type theory.
Evan Cavallo, Anders Mörtberg, & Andrew W Swan.
To appear in Computer Science Logic (CSL) 2020.
[Paper] [Technical report: type theory] [Technical report: model structure] [Agda]
19.01 | Higher inductive types in cubical computational type theory.
Evan Cavallo & Robert Harper.
Principles of Programming Languages (POPL) 2019.
[Paper] [Technical 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]
15.12 | Synthetic cohomology in homotopy type theory.
Master's thesis in Mathematical Sciences @ Carnegie Mellon U.
[Thesis]

Preprints & notes


19.10 | "Stable factorization from a fibred algebraic weak factorization system".
Evan Cavallo.
[arXiv preprint]
19.06 | "Model structures on cubical sets".
Evan Cavallo, Anders Mörtberg, & Andrew W Swan.
[Note]
19.02 | "A unifying cartesian cubical type theory".
Evan Cavallo & Anders Mörtberg.
[Note]
19.01 | "Parametric cubical type theory".
Evan Cavallo & Robert Harper.
[arXiv preprint]
18.01 | "Computational higher type theory IV: Inductive types".
Evan Cavallo & Robert Harper.
[arXiv preprint]

Talks


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.
you must scream to your target, you must use other language than yours