Skip to content

Curriculum vitae

Download PDF

williamdemeo@gmail.com · williamdemeo.org

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.

Theory. Universal algebra, logic, lattice theory, proof theory, category theory, type theory, complexity theory, algorithmic complexity, machine learning.

Practice. Proof mechanization in Agda and Lean, computer-aided mathematics, formal verification, functional programming for AI, ML and Big Data in Scala/Spark.

Education

2012
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
Formal verification of the Cardano blockchain ledger specification in Agda. 2 years.
Project
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.
AFOSR · Haleakala Observatories · MHPCC

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

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

  • Smart Contracts
    SUNY at Buffalo, 4-week Coursera course, 96.4%, 5 Sep 2021 · Certificate

  • Blockchain Basics
    SUNY at Buffalo, 4-week Coursera course, 100%, 6 Aug 2021 · Certificate

  • Big Data Analysis with Scala and Spark
    Ecole Polytechnique Federale de Lausanne, 4-week Coursera course, 93.4%, 24 Nov 2017 · Certificate

  • Functional Programming Principles in Scala
    Ecole Polytechnique Federale de Lausanne, 6-week Coursera course, 100%, 17 Nov 2016 · Certificate

  • Functional Program Design in Scala
    Ecole Polytechnique Federale de Lausanne, 4-week Coursera course, 100%, 6 Aug 2016 · Certificate

  • Parallel Programming in Scala
    Ecole Polytechnique Federale de Lausanne, 4-week Coursera course, 100%, 27 Jun 2016 · Certificate

  • Startup Engineering
    Stanford University, 12-week Coursera course, 99.3%, 23 Sep 2013 · Certificate

Summer schools and short courses

References

  • Clifford Bergman, Professor 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, Assistant Professor of Mathematics, University of Colorado, Boulder (teaching reference)

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