Reed Mullanix

About Me:

I'm a graduate student at McMaster University studying under Dr. Jacques Carette. Previously, I was a research programmer affiliated with the University of Minnesota working 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 techniques 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 leaves a lot to be desired, and I believe 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'm interested in how we can automate away tricky coherence problems to alleviate some of the machine-induced suffering.

I hold a BSc in Computer Science from the University of British Columbia. My other interests include bouldering, cycling, and running. I've also run every street in my hometown of Santa Barbara, CA!