Skip to content

Curriculum vitae

Download PDF

williamdemeo@gmail.com · williamdemeo.github.io

Research interests

What mathematics is mechanizable and which machine-checked results can we trust? These questions have become the throughline of my work on the following: congruence lattices of finite algebras and the finite lattice representation problem; algebraic approaches to the complexity of constraint satisfaction problems; formalization of mathematics in dependent type theory; formal methods for a production blockchain ledger; AI agents that work inside a proof assistant, where the typechecker is the verifiable reward signal.

Theory. Universal algebra and lattice theory, and the algebraic theory of constraint-satisfaction complexity that grew out of them; constructive dependent type theory as a foundation for machine-checked mathematics; and proof search with the typechecker as the only judge, including what its verdicts can and cannot teach a learned policy.

Practice. Proof mechanization in Agda, in a research library and in a production specification; and the infrastructure that lets language models work inside a proof assistant, built so that every claim about it is a measurement someone else can reproduce.

Education

Doctor of Philosophy in Mathematics, University of Hawaii, Honolulu
Thesis: Congruence lattices of finite algebras.
Advisor: Ralph Freese.

Master of Science in Mathematics, Courant Institute of Mathematical Sciences, NYU, New York
Thesis: Approximating eigenvalues of large stochastic matrices.
Advisor: Jonathan Goodman.

Bachelor of Arts in Economics, University of Virginia, Charlottesville

Appointments

2023–
Formal Verification Engineer, Formal Methods Team, IO, Boulder
Machine-checked specification of the Cardano blockchain ledger in Agda, with the Formal Methods team. The specification is literate Agda: the human-readable ledger specification is generated from it, and Haskell is extracted from it and run in conformance tests against the production implementation, so it has to type-check, compile, and agree with a separately written system that live nodes run. It tracks the chain across its eras, the Conway era complete and Dijkstra in progress. The largest single share of commits in the repository's history; the design is described in the FMBC 2024 paper below.
Project · Specification · Contributors
2022–2023
Senior University Lecturer, Computer Science Dept., New Jersey Inst. of Technology, Newark
Taught courses in foundations of computing, big data, and artificial intelligence. 18 months.
2022–2023
Software Engineer, Library Team, RelationalAI, New York
Developed the Standard Library of the Rel declarative programming language. 9 months.
2019–2021
Postdoctoral Research Fellow, Algebra Dept., Charles University, Prague
2017–2019
Burnett Meyer Instructor, Mathematics Dept., University of Colorado, Boulder
2016–2017
Visiting Assistant Professor, Mathematics Dept., University of Hawaii, Honolulu
2014–2016
Postdoctoral Associate, Mathematics Dept., Iowa State University, Ames
2012–2014
Visiting Assistant Professor, Mathematics Dept., Univ South Carolina, Columbia
2001–2006
Senior Research Scientist, Imaging Research Dept., Textron Systems Corp., Maui
Worked full-time on AFOSR contracts developing new algorithms and parallel (smp and mpi) programs for processing images acquired by the Haleakala Observatories, including Multi-frame Blind Deconvolution for removing the distorting effects of Earth's atmosphere from images of satellites and other NEOs; executed our programs on the MHPCC supercomputer.
Haleakala Observatories

Grants and awards

2015–2018
NSF Research Grant no. 1500218
Algebras and algorithms, structure and complexity theory.
Postdoctoral research fellow on a team with 6 senior scientists and 3 postdocs.
3-yr collaborative research on algebraic approaches to constraint satisfaction problems.
2013–2014
Magellan Scholar Grant
What does a nonabelian group sound like?
Faculty mentor for undergraduate research.
2011
ARCS Sarah Ann Martin Award for Outstanding Research in Mathematics, Honolulu
2004
Best Paper Award, International Symposium on Musical Acoustics, Nara, Japan

Selected publications

  1. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda
    Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell.
    5th International Workshop on Formal Methods for Blockchains (FMBC 2024), OASIcs Volume 118, 2024, pages 2:1-2:18.
    Proceedings

  2. Universal algebraic methods for constraint satisfaction problems
    Clifford Bergman and William DeMeo.
    Logical Methods in Computer Science (LMCS), Volume 18, Issue 1, 2022.
    Journal · arXiv preprint

  3. A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory
    William DeMeo and Jacques Carette.
    27th International Conference on Types for Proofs and Programs (TYPES 2021), LIPIcs Volume 239, 2022, pages 4:1-4:21.
    Proceedings · arXiv preprint

  4. Constraint satisfaction problems over finite structures
    Libor Barto, William DeMeo, and Antoine Mottet.
    36th ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), Rome, Italy, 2021, pages 1-13.
    Proceedings · arXiv preprint

  5. Bounded homomorphisms and finitely generated fiber products of lattices
    William DeMeo, Peter Mayr, and Nik Ruškuc.
    International Journal of Algebra and Computation (IJAC), Volume 30, Issue 4, 2020, pages 693-710.
    Journal · arXiv preprint

  6. Polynomial-time tests for difference terms in idempotent varieties
    William DeMeo, Ralph Freese, and Matthew Valeriote.
    International Journal of Algebra and Computation (IJAC), Volume 29, Issue 6, 2019, pages 927-949.
    Journal · arXiv preprint

The complete record, with abstracts, is on the publications page.

Projects

  • AI for formal verification (agda-native-air)
    Principal author; active since 2025.
    Infrastructure that lets language models work inside the Agda proof assistant with the typechecker as the oracle and final arbiter of truth. agda-mcp is a server that exposes Agda's interaction protocol to coding agents under a verdict discipline: every verdict is derived from a batch Agda process's exit code and travels with the command it is equivalent to, while a persistent interaction lane answers questions in milliseconds and never decides. A proof-search loop drives that server with Agda judging every step. Structured extraction turns whole libraries into released corpora with recorded provenance, and benchmark tests against gold solutions with per-run honesty ledgers make every claim about the loop reproducible. The tooling was the instrument for a new machine-checked formal proof of the Kurzweil–Netter duality theorem in agda-algebras.
    Releases · Benchmark · Proof search (ADR 0001) · agda-mcp (ADR 0002) · Field reports · Kurzweil–Netter

  • The Agda Universal Algebra Library (agda-algebras)
    With Jacques Carette.
    Active since 2019.
    A formalization of universal algebra in Agda, in constructive Martin-Löf type theory with no classical axioms: general algebras, homomorphisms, congruences, terms, varieties, and the equational logic and model theory beneath them. Its flagship result is a fully constructive machine-checked proof of Birkhoff's HSP theorem that postulates no function extensionality (TYPES 2021, below). About 300 literate modules and 60,000 lines of Agda, type-checked in CI against Agda 2.8.0; the documentation site publishes its own size. Now also the substrate for a machine-checked research program on the finite lattice representation problem.
    Documentation · Birkhoff's HSP theorem

  • Category Theory: a concise course
    With Charlotte Aten and Venanzio Capretta.
    Work in progress.

  • Complex Analysis Exams
    Work in progress.

  • Real Analysis Exams
    Work in progress.

Teaching

New Jersey Institute of Technology, Senior University Lecturer

  • DS 644 Introduction to Big Data, graduate course, Spring 2023
  • CS 644 Introduction to Big Data, graduate course, Fall 2022
  • CS 370 Introduction to Artificial Intelligence, Fall 2022
  • CS 370 Introduction to Artificial Intelligence, Spring 2022
  • CS 241 Foundations of Computer Science I, Spring 2022

Charles University in Prague, Postdoctoral Research Fellow

  • NMAG 405 Universal Algebra, Winter 2020

University of Colorado, Boulder, Burnett Meyer Instructor

  • Math 2001 Discrete Mathematics, with Lean prover component, Spring 2019
  • Math 2001 Discrete Mathematics, with Lean prover component, Fall 2018
  • Math 3140 Abstract Algebra, Fall 2018
  • Math 6000 Model Theory, graduate course, Spring 2018
  • Math 2130 Linear Algebra, Spring 2018
  • Math 2130 Linear Algebra, Fall 2017

University of Hawaii, Visiting Assistant Professor

  • Math 215 Applied Calculus, Spring 2017
  • Math 480 Senior Seminar, Spring 2017
  • Math 244 Calculus IV, Fall 2016
  • Math 321 Introduction to Advanced Math, Fall 2016

Iowa State University, Postdoctoral Associate

  • Math 317 Linear Algebra, Spring 2016
  • Math 317 Linear Algebra, Fall 2015
  • Math 160 Survey of Calculus, Fall 2015
  • Math 207 Elementary Linear Algebra, Spring 2015
  • Math 165 Calculus I, Spring 2015
  • Math 301 Abstract Algebra, Fall 2014
  • Math 165 Calculus I, Fall 2014

University of South Carolina, Visiting Assistant Professor

  • Math 700 Linear Algebra, graduate course, Spring 2014
  • Math 141 Calculus I, Spring 2014
  • Math 374 Discrete Structures, Fall 2013
  • Math 122 Calculus for Business and Social Sciences, Fall 2013
  • Math 374 Discrete Structures, Spring 2013
  • Math 122 Calculus for Business and Social Sciences, Spring 2013
  • Math 241 Vector Calculus, Fall 2012
  • Math 122 Calculus for Business and Social Sciences, Fall 2012

University of Hawaii, Graduate Student Instructor

  • Math 371 Probability Theory, Summer 2011
  • Math 100 Mathematical Reasoning, Summer 2010
  • Math 215 Applied Calculus I, Summer 2009

Talks

Service

  • Organizer, BLAST 2019 Conference, Boulder, 2019

  • Organizer, Algebras and Lattices in Hawaii Conference, to honor Freese, Lampe & Nation, Honolulu, 2018

  • Organizer, Workshop on Computational Universal Algebra, Louisville, 2013

  • Editor, Algebra Universalis, 2018–

  • Referee, Algebra Universalis, Order, and J. Logic & Analysis, 2012–

  • Graduate Student Representative, Working Group on Graduate Education, University of Hawaii
    Graduate Student Representative on a committee of deans and department heads; helped draft a resolution for the Committee on Research and Graduate Education.

  • Faculty Senate Student Rep., Academic Committee Chair, Math Department Rep., Graduate Student Organization, University of Hawaii

  • Mentor for Undergraduate Research, Mathematical Biology Program, University of Hawaii
    Mentored students in math and dsp for classifying marine life audio signals.

Advising and mentoring

  • University of Colorado, Boulder
    Served on the doctoral candidacy exam committee for the following ph.d. students: Jordan DuBeau, Ali Lotfi, Athena Sparks, Michael Wheeler. Served on the dissertation defense committee for Jeffrey Shriner.

  • Iowa State University
    REU mentor for Charlotte Aten (mathematics major, University of Rochester); honors thesis advisor for Joshua Thompson (mathematics major, honors program); Putnam Exam mentor at weekly exam practice meetings; Undergraduate Tea cohost of weekly undergraduate student gatherings; Iowa 4-H Youth Conference volunteer mentor.
    Link

  • University of South Carolina
    Honors thesis mentor for Matthew Corley (computer science major, honors program); South Carolina High School Math Contest exam design committee; Faculty mentor for Pi Mu Epsilon (math honors society).

Certifications

  • Selected online coursework
    Coursera certificates in Smart Contracts and Blockchain Basics (SUNY at Buffalo, 2021); Big Data Analysis with Scala and Spark, Functional Programming Principles in Scala, Functional Program Design in Scala, and Parallel Programming in Scala (EPFL, 2016 and 2017); and Startup Engineering (Stanford University, 2013).

Summer schools and short courses

References

  • Clifford Bergman, Professor Emeritus of Mathematics, Iowa State University (teaching reference)

  • Venanzio Capretta, Assistant Professor of Computer Science, University of Nottingham

  • Ralph Freese, Professor of Mathematics, University of Hawaii

  • Peter Jipsen, Professor of Mathematics, Chapman University

  • George McNulty, Professor of Mathematics, University of South Carolina

  • Peter Mayr, Professor of Mathematics, University of Colorado, Boulder (teaching reference)

  • J.B. Nation, Emeritus Professor of Mathematics, University of Hawaii