Skip to content

Curriculum vitae

Download PDF

This page is a summary, and the PDF is out of date

The linked PDF predates the current role and does not mention any of the recent work on AI tooling for proof assistants. Both are being replaced by a single source that renders to web and PDF together (#41), with the content brought current in #42. Full talks and teaching records arrive with Milestone 5.

Research interests

Interactive theorem proving and formalization of mathematics (Agda, Lean); formal methods for production systems; AI tooling for proof assistants and machine reasoning over verifiable domains; universal algebra, lattice theory, and the algebraic approach to computational complexity.

Education

PhD, Mathematics — University of Hawaii, 2012
Thesis: Congruence lattices of finite algebras. Advisor: Ralph Freese.
MS, Mathematics — Courant Institute of Mathematical Sciences, NYU
Thesis: Approximating eigenvalues of large stochastic matrices. Advisor: Jonathan Goodman.

BA, Economics — University of Virginia

Employment

See the about page for the full table. Current position: Formal Verification Engineer, Formal Methods team, IO, since 2023 — formal verification of the Cardano blockchain ledger specification in Agda.

Selected publications

  1. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda, with Knispel et al. 5th International Workshop on Formal Methods for Blockchains (FMBC), 2024. DOI

  2. A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory, with Jacques Carette. 27th International Conference on Types for Proofs and Programs (TYPES), 2022. arXiv:2101.10166

  3. Universal algebraic methods for constraint satisfaction problems, with Clifford Bergman. Logical Methods in Computer Science (LMCS), 2022. Journal

  4. Constraint satisfaction problems over finite structures, with Libor Barto and Antoine Mottet. 36th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021. arXiv:2010.04958

  5. Bounded homomorphisms and fiber products of lattices, with Peter Mayr and Nik Ruškuc. International Journal of Algebra and Computation (IJAC), 2020. arXiv:1907.08046

  6. Polynomial-time tests for difference terms in idempotent varieties, with Ralph Freese and Matthew Valeriote. International Journal of Algebra and Computation (IJAC), 2019. arXiv:2011.07879

The complete list, including earlier work in algebra and in signal processing, is on arXiv and in the PDF. A generated, single-source publications page arrives with Milestone 5 (#29).

Grants and awards

NSF Research Grant no. 1500218 (2015–2018)
Algebras and algorithms, structure and complexity theory. Postdoctoral research fellow on a team of six senior scientists and three postdocs; collaborative research on algebraic approaches to constraint satisfaction.
Magellan Scholar Grant (2013–2014)
Faculty mentor for undergraduate research.

ARCS Sarah Ann Martin Award for outstanding research in mathematics (2011)

Best Paper Award, International Symposium on Musical Acoustics, Nara, Japan (2004)

Teaching

A decade of teaching across six institutions, from calculus through graduate model theory, including courses that used the Lean proof assistant in an undergraduate discrete mathematics classroom. The full record arrives with Milestone 5 (#32).