Evan Cavallo

I am 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.

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.

19.03  |  HoTTEST: parametric cubical type theory - slides, video
19.01  |  POPL 2019: higher inductive types in cubical computational type theory - slides, video
18.03  |  MURI grant meeting: computational interpretation of cubical inductive types - slides
17.03  |  MURI grant meeting: relative Kan completion in a nominal sets model - notes
14.09  |  Oxford HoTT Workshop: the Mayer-Vietoris sequence and cubes - 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, 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