evan cavallo


I'm a 4th-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.


works


????? | Cavallo & Harper. Internal parametricity for cubical type theory. In preparation.
????? | Cavallo, Mörtberg, & Swan. Unifying cubical models of univalent type theory. In preparation.
19.01 | Cavallo & Harper. Higher inductive types in cubical computational type theory. POPL 2019.
18.07 | Angiuli, Cavallo, Favonia, Harper, & Sterling. The RedPRL proof assistant. LFMTP 2018.
15.12 | Cavallo. Synthetic cohomology in homotopy type theory. Master's thesis.

preprints & notes


19.02 | Cavallo & Mörtberg. A unifying cartesian cubical type theory.
19.01 | Cavallo & Harper. Parametric cubical type theory.
18.01 | Cavallo & Harper. Computational higher type theory IV: Inductive types.

acts


19.06 | HoTT-UF: cubical indexed inductive types - slides
19.06 | TYPES: internally parametric cubical type theory - slides
19.03 | HoTTEST: parametric cubical type theory - slides, video
19.01 | POPL: higher inductive types in cubical computational type theory - slides, video
14.09 | Oxford HoTT Workshop: the Mayer-Vietoris sequence and cubes - 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, CMU Computer Science Dept
10-15 | undergraduate & honors master's student, CMU Math Dept


Address mail to ecavallo, zip code cs.cmu.edu; alternatively, GHC 9223
you must scream to your target, you must use other language than yours