evan cavallo

I'm 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.

works

?????	\|	Cavallo & Harper. Internal parametricity for cubical type theory. In preparation.
?????	\|	Cavallo, Mörtberg, & Swan. Unifying cubical models of univalent type theory. In preparation.
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.06	\|	HoTT-UF: cubical indexed inductive types - slides
19.06	\|	TYPES: internally parametric cubical type theory - slides
19.03	\|	HoTTEST: parametric cubical type theory - slides, video
19.01	\|	POPL: higher inductive types in cubical computational type theory - slides, video
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