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