I'm a postdoctoral fellow in the
division of
the Department of Mathematics
at Stockholm University. Before that I was a Ph.D. student in
computer science at Carnegie Mellon
University under Robert
Harper. I study type theories with interval structure,
particularly cubical type theory and internally parametric type
theory.
Address mail to evan.cavallo, postal code math.su.se.
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] |
21.02 | | |
Higher inductive types and internal parametricity for cubical type theory.. Ph.D. thesis in Computer Science @ Carnegie Mellon U. Evan Cavallo. [CMU Technical Report] (revised May 2021: errata) |
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] |
agda/cubical [Github] – contributor A library for the --cubical mode of the Agda proof assistant. |
ptt [Github] – creator An experimental implementation of a type-checker for a type theory with internal parametricity, using Gratzer, Sterling, and Birkedal's blott as a base. |
redtt & RedPRL [Website] – contributor Proof assistants for cartesian cubical type theory. |
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] |
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. |
21-?? | | | Postdoctoral Fellow in Computational Mathematics @ Stockholm U. |
15-21 | | | Ph.D. student in Computer Science @ Carnegie Mellon U. |
10-15 | | | Undergraduate & Honors Master's student in Mathematical Sciences @ Carnegie Mellon U. |