Who am I?

Jack Gallagher - mathematician, type theorist, and programmer - not always in that order. You can find more (if somewhat outdated) details in this post.

Contact Info

The best way to reach me is by . You can also find me on Github, and of course on this blog.

What I’m up to these days

I’m currently a research contractor at the Machine Intelligence Research Institute, where I’m working on building tools for doing reflection in different type theories, with the eventual goal of being able to formalize all of MIRI’s work. Sometimes this means object-level formalization work (as in the implementation of Botworld in HOL, and my formalizations of dependently typed syntax), and sometimes it means developing more general tools for automatic formalization.


Things I wrote (mostly) on my own

Other projects I’ve contributed to