Reed MullanixEmail: firstname.lastname@example.org
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!
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.
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.