I'm a postdoctoral fellow in the
Computational
Mathematics division
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 primitive higher-dimensional structure, particularly cubical and internally
parametric type theories. I am exploring the features we can build into these theories (e.g., higher
inductive types), exploring what we can do inside them (e.g., proving coherence theorems with
parametricity), and attempting to make systematic sense of the wild world of type theories based on
different cubical structures.
Address mail to evan.cavallo, postal code math.su.se.
22.05 | | |
Modalities and parametric adjoints. Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, & Lars Birkedal. Transactions on Computational Logic. [Paper] |
21.11 | | |
Internal parametricity for cubical type theory. Evan Cavallo & Robert Harper. Logical Methods in Computer Science. Extended version of CSL 2020 paper. [Paper] [arXiv] |
21.01 | | |
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) |
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] – co-maintainer 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. |
21.12 | | | Another model structure presenting spaces from a cubical type theory. @ Stockholm-Göteborg joint seminar. [Slides] |
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] |
22.Sp | | | Teacher for DA2005 Programming techniques |
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. |