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¶
One question runs through the work: what mathematics is mechanizable, and which machine-checked results can we trust? It began in universal algebra and lattice theory, ran through the algebraic approach to computational complexity, into the formalization of universal algebra in dependent type theory, into the machine-checked specification of a production ledger, and now into tooling that lets language models work inside a proof assistant. Research tells that story and says what comes next; the projects carry the evidence.
Employment record¶
| 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.