About¶
I am a mathematician working as a formal verification engineer on the Formal Methods team at IO, where I work on the machine-checked specification of the Cardano blockchain ledger in Agda.
Before that I spent a decade in academia. I hold a PhD in mathematics from the University of Hawaii, where I worked on universal algebra and lattice theory under Ralph Freese; my thesis was on congruence lattices of finite algebras. I also hold an MS in mathematics from the Courant Institute at NYU, where I worked with Jonathan Goodman on numerical methods for large stochastic matrices, and a BA in economics from the University of Virginia.
What I work on¶
My research has moved along a fairly consistent line, even though the subject labels have changed several times.
It began in universal algebra and lattice theory — congruence lattices of finite algebras, and the finite lattice representation problem. That led to the algebraic approach to computational complexity, where the tractability of a constraint satisfaction problem is determined by the algebraic structure of its template, and to work with Libor Barto, Antoine Mottet, and Clifford Bergman on CSPs over finite and infinite structures.
Wanting those arguments to be checkable rather than merely careful took me into formalization of mathematics in dependent type theory, and to agda-algebras — a library of universal algebra in Agda, which contains a machine-checked proof of Birkhoff's HSP theorem in Martin-Löf type theory, joint with Jacques Carette.
That in turn led to formal methods in industry: specifying a production blockchain ledger in Agda is a different discipline from formalizing a textbook theorem, because the specification has to track a system under active development and stay readable by engineers who are not type theorists.
Most recently I have been building AI tooling for interactive theorem proving — infrastructure that lets language models work inside a proof assistant, and the question of what a typechecker's verifiable feedback makes possible that unverifiable domains do not.
Academic appointments¶
| Years | Position | Institution |
|---|---|---|
| 2023– | Formal Verification Engineer, Formal Methods | IO |
| 2022–2023 | Senior University Lecturer, Computer Science | NJIT |
| 2022–2023 | Software Engineer, Library Team | RelationalAI |
| 2019–2021 | Postdoctoral Research Fellow, Algebra | Charles University, Prague |
| 2017–2019 | Burnett Meyer Instructor, Mathematics | University of Colorado Boulder |
| 2016–2017 | Visiting Assistant Professor, Mathematics | University of Hawaii |
| 2014–2016 | Postdoctoral Associate, Mathematics | Iowa State University |
| 2012–2014 | Visiting Assistant Professor, Mathematics | University of South Carolina |
| 2001–2006 | Research Scientist, Imaging Research | Textron Systems |
Service¶
Editor for Algebra Universalis since 2018, and a referee for Algebra Universalis, Order, and the Journal of Logic and Analysis. I have organised several conferences, including BLAST 2019 in Boulder and Algebras and Lattices in Hawaii 2018, which honoured Ralph Freese, Bill Lampe, and J.B. Nation.
Elsewhere¶
The CV has the full record. Contact has ways to reach me and links to my code and publications.