Evan Cavallo
I am a postdoc in the
Logic and Types group
at Göteborgs universitet
under Thierry Coquand. Previously I was a postdoc in
the
Computational
Mathematics division
at Stockholms universitet under Anders Mörtberg, and before that I was a Ph.D. student in
computer science at Carnegie Mellon
University under Robert Harper.
I study constructive type theories, particularly new ways to treat proofs as constructions. My
current research focuses on the constructive reading of proofs of equality as paths in space,
which is the basis of cubical type theories. I am developing extensions to these theories (such
as higher inductive types and internal parametricity), exploring their applications (such as
for representation independence), studying their connections to homotopy theory, and working to
systematize their design.
Address mail to evan.cavallo, postal code gu.se.
I am @ecavallo@mathstodon.xyz on Mastodon.
Latest:
- A talk at HoTT Electronic Seminar Talks on cubical models that don't present spaces.
- A preprint with Maximilian Doré and Anders Mörtberg on automation for higher-dimensional reasoning in cubical type theories.
Publications
| 22.05 | | |
Modalities and parametric adjoints. Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, & Lars Birkedal. Transactions on Computational Logic (TOCL). [DOI] [local copy] |
| 21.11 | | |
Internal parametricity for cubical type theory. Evan Cavallo & Robert Harper. Logical Methods in Computer Science (LMCS). Extended version of CSL 2020 paper. [DOI] [arXiv] |
| 21.01 | | |
Internalizing representation independence with univalence. Carlo Angiuli, Evan Cavallo, Anders Mörtberg, & Max Zeuner. Principles of Programming Languages (POPL) 2021. [DOI] [local copy] [formalization] (errata) |
| 20.01 | | |
Internal parametricity for cubical type theory. Evan Cavallo & Robert Harper. Computer Science Logic (CSL) 2020. [DOI] [local copy] [tech report] |
| 20.01 | | |
Unifying cubical models of univalent type theory. Evan Cavallo, Anders Mörtberg, & Andrew W Swan. Computer Science Logic (CSL) 2020. [DOI] [local copy] [tech report: type theory] [tech report: model structure] [formalization] |
| 19.01 | | |
Higher inductive types in cubical computational type theory. Evan Cavallo & Robert Harper. Principles of Programming Languages (POPL) 2019. [DOI] [local copy] [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. [DOI] [arXiv] |
Preprints, notes, &c.
| 24.02 | | |
Automating boundary filling in Cubical Agda. Maximilian Doré, Evan Cavallo, & Anders Mörtberg. Submitted. [arXiv] |
| 22.11 | | |
Relative elegance and cartesian cubes with one connection. Evan Cavallo and Christian Sattler. Preprint. [arXiv] |
| 21.02 | | |
Higher inductive types and internal parametricity for cubical type theory. Evan Cavallo. Ph.D. thesis in Computer Science @ Carnegie Mellon U. [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. [local copy] |
Code
|
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. |
Selected talks
| 24.03 | | | Why some cubical models don't present spaces. @ HoTT Electronic Seminar Talks [slides] [video] |
| 22.11 | | | Cubes with one connection and relative elegance. @ HoTT Electronic Seminar Talks [slides] [video] |
| 21.04 | | | Fitch-style modalities and parametric adjoints. @ 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 [slides] |
| 19.06 | | | Internally parametric cubical type theory. @ TYPES 2019 [slides] |
| 19.03 | | | Parametric cubical type theory. @ HoTT Electronic Seminar Talks [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] |
Teaching
| 24.Sp | | | TA for DAT280/DIT261 Parallel functional programming |
| 24.Sp | | | TA for TDA342 Advanced functional programming |
| 23.Sp | | | Instructor for DA2005 Programming techniques |
| 22.Fa | | | Instructor for DA2005 Programming techniques |
| 22.Sp | | | Instructor 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 |
Status
| 23– | | | Postdoc in Logic and Types @ Göteborgs U. |
| 21–23 | | | Postdoc in Computational Mathematics @ Stockholms 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. |