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.

works:

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.

records:

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

teaching:

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

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