Reed Mullanix


About Me:

I'm a research programmer affiliated with the University of Minnesota, working on as a member of the RedPRL development team. My main research interest is the intersection between higher-dimensional type theories and proof assistant usability, focusing on how we can use the tools of cubical type theory to smooth over some of the sharp edges of existing tools.

I'm also very interested in the theory of dependent record types. As it stands, using records in most proof assistants leads a lot to be desired, and I think that the experience could be radically improved.

Finally, I have a long-running interest in mechanized category theory, and contribute to both agda-categories and the 1Lab. In particular, I am interested in how we can apply the tools of proof automation to tricky coherence problems to try and reduce some of the machine-induced suffering.

I have a BSc in Computer Science from UBC. My other interests include bouldering, cycling, and running. I've run every street in Santa Barbara, CA!


Workshop Talks