Evan Cavallo

I am a fourth-year Ph.D. student in Computer Science at Carnegie Mellon University, part of the Principles of Programming group. I am advised by Robert Harper and work on cubical type theories and their ilk.

19.01 Cavallo and Harper. Higher inductive types in computational cubical type theory. POPL'19.
18.07 Angiuli, Cavallo, Favonia, Harper, & Sterling. The RedPRL proof assistant. LFMTP'18.
18.01 Cavallo and Harper. Computational higher type theory IV: Inductive types. arXiv preprint.
15.12 Cavallo. Synthetic cohomology in homotopy type theory. Master's thesis.
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.F - TA for 15-317 Constructive Logic
15.F - TA for 15-814 Types and Programming Languages
15.S - TA for 15-312 Foundations of Programming Languages
14.F - 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