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.
| 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] |
| 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] |
| 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. |
| 15-?? | | | Ph.D. student in Computer Science @ Carnegie Mellon U. |
| 10-15 | | | Undergraduate & Honors Master's student in Mathematical Sciences @ Carnegie Mellon U. |