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

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