Reed Mullanix
Email: reedmullanix@gmail.comGithub: https://github.com/totbwf
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!
Papers
Projects
Workshop Talks
-
WITS '22: Setting The Record Straight with Singletons [Recording]
I discussed a solution to the "bundling" problem of record types in dependent type theory, and presented a lightweight solution that leveraged singleton types.
Presentations
-
MURI '23: Directed Cooltt
I discussed progress on adding cooltt, some challenges encountered, and insights gained along the way.
-
MURI '22: A Universal Algebraic Approach to Universes
I presented joint work with Favonia and Carlo Anguili on universe levels.
-
MURI '21: What's Cool about Cooltt
I discussed some of the unique features of cooltt, and explored how we can leverage cubical type theory to improve the experience of actually using a proof assistant.
-
Boston Haskell: Programming with Tactics [Recording]
I discussed how refinery is implemented, and how it is used inside of the Haskell Language Server to power its program synthesis engine.