Skip to content

Publications

Universal algebra and lattice theory, constraint satisfaction, formal verification in Agda, and — earlier — signal processing. Everything below is generated from one file, checked against the publishers that hold the records; ADR-006 says how.

Each entry links whatever exists for it: the version of record, the arXiv preprint, or — for most — both, side by side. A few have neither, and say so by carrying no link rather than by pointing somewhere that does not answer. The whole list is also available as BibTeX.

Selected

The work most relevant to formal verification and to the roles described on the CV, linked into the full record below.

Journal articles

  • Universal algebraic methods for constraint satisfaction problems
    Clifford Bergman and William DeMeo.
    Logical Methods in Computer Science (LMCS), Volume 18, Issue 1, January 19, 2022. doi:10.46298/lmcs-18(1:12)2022
    Journal · arXiv preprint

    Abstract

    After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if the algebra has a Taylor term operation. Despite the tremendous achievements in this area (including recently announce proofs of the general conjecture), there remain examples of small algebras with just a single binary operation whose CSP resists direct classification as either tractable or NP-complete using known methods. In this paper we present some new methods for approaching such problems, with particular focus on those techniques that help us attack the class of finite algebras known as "commutative idempotent binars" (CIBs). We demonstrate the utility of these methods by using them to prove that every CIB of cardinality at most 4 yields a tractable CSP.

  • 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, June 2020, pages 693-710. doi:10.1142/S0218196720500174
    Journal · arXiv preprint

    Abstract

    We investigate when fiber products of lattices are finitely generated and obtain a new characterization of bounded lattice homomorphisms onto lattices satisfying a property we call Dean's condition (D) which arises from Dean's solution to the word problem for finitely presented lattices. In particular, all finitely presented lattices and those satisfying Whitman's condition satisfy (D). For lattice epimorphisms \(g\colon A\to D\), \(h\colon B\to D\), where \(A\), \(B\) are finitely generated and \(D\) satisfies (D), we show the following: If \(g\) and \(h\) are bounded, then their fiber product (pullback) \(C=\{(a,b)\in A\times B\ |\ g(a)=h(b)\}\) is finitely generated. While the converse is not true in general, it does hold when \(A\) and \(B\) are free. As a consequence we obtain an (exponential time) algorithm to decide boundedness for finitely presented lattices and their finitely generated sublattices satisfying (D). This generalizes an unpublished result of Freese and Nation.

  • 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, September 2019, pages 927-949. doi:10.1142/S021819671950036X
    Journal · arXiv preprint

    Abstract

    We consider the following practical question: given a finite algebra A in a finite language, can we efficiently decide whether the variety generated by A has a difference term? We answer this question (positively) in the idempotent case and then describe algorithms for constructing difference term operations.

  • Isotopic algebras with nonisomorphic congruence lattices
    William DeMeo.
    Algebra universalis, Volume 72, Issue 3, November 2014, pages 295-298. doi:10.1007/s00012-014-0301-4
    Journal · arXiv preprint

    Abstract

    We give examples of pairs of isotopic algebras with non-isomorphic congruence lattices. This answers the question of whether all isotopic algebras have isomorphic congruence lattices.

  • Expansions of finite algebras and their congruence lattices
    William DeMeo.
    Algebra universalis, Volume 69, Issue 3, May 2013, pages 257-278. doi:10.1007/s00012-013-0226-3
    Journal · arXiv preprint

    Abstract

    We present a novel approach to the construction of new finite algebras and describe the congruence lattices of these algebras. Given a finite algebra \((B_0, \dots)\), let \(B_1, B_2, \dots, B_K\) be sets that either intersect \(B_0\) or intersect each other at certain points. We construct an \emph{overalgebra} \((A, F_A)\), by which we mean an expansion of \((B_0, \dots)\) with universe \(A = B_0 \cup B_1 \cup \cdots \cup B_K\), and a certain set \(F_A\) of unary operations that includes mappings \(e_i\) satisfying \(e_i^2 = e_i\) and \(e_i(A) = B_i\), for \(0\leq i \leq K\). We explore two such constructions and prove results about the shape of the new congruence lattices \(Con(A, F_A)\) that result. Thus, descriptions of some new classes of finitely representable lattices is one contribution of this paper. Another, perhaps more significant contribution is the announcement of a novel approach to the discovery of new classes of representable lattices, the full potential of which we have only begun to explore.

Conference and workshop papers

  • 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, May 21, 2024, pages 2:1-2:18. doi:10.4230/OASIcs.FMBC.2024.2
    Proceedings

    Abstract

    Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.

  • 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, August 4, 2022, pages 4:1-4:21. doi:10.4230/LIPIcs.TYPES.2021.4
    Proceedings · arXiv preprint

    Abstract

    The Agda Universal Algebra Library is a project aimed at formalizing the foundations of universal algebra, equational logic and model theory in dependent type theory using Agda. In this paper we draw from many components of the library to present a self-contained, formal, constructive proof of Birkhoff’s HSP theorem in Martin-Löf dependent type theory. This achieves one of the project’s initial goals: to demonstrate the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures by using them to formalize a significant theorem in the field.

  • 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, June 29, 2021, pages 1-13. doi:10.1109/LICS52264.2021.9470670
    Proceedings · arXiv preprint

    Abstract

    We initiate a systematic study of the computational complexity of the Constraint Satisfaction Problem (CSP) over finite structures that may contain both relations and operations. We show the close connection between this problem and a natural algebraic question: which finite algebras admit only polynomially many homomorphisms into them? We give some sufficient and some necessary conditions for a finite algebra to have this property. In particular, we show that every finite equationally nontrivial algebra has this property which gives us, as a simple consequence, a complete complexity classification of CSPs over two-element structures, thus extending the classification for two-element relational structures by Schaefer (STOC'78). We also present examples of two-element structures that have bounded width but do not have relational width (2,3), thus demonstrating that, from a descriptive complexity perspective, allowing operations leads to a richer theory.

  • Topics in nonabelian harmonic analysis and DSP applications
    William DeMeo. Best paper award.
    Proceedings of the International Symposium on Musical Acoustics (ISMA 2004), Nara, Japan, 2004.
    PDF

  • Characterizing musical signals with Wigner-Ville interferences
    William DeMeo.
    Proceedings of the International Computer Music Conference (ICMC 2002), Gothenburg, Sweden, 2002.

  • Approximating eigenvalues of large stochastic matrices
    William DeMeo.
    Proceedings of the 8th Copper Mountain Conference on Iterative Methods, Copper Mountain, Colorado, 1998.
    Link

Preprints and unpublished manuscripts

  • A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory
    William DeMeo and Jacques Carette. Unabridged 35-page version.
    arXiv preprint arXiv:2101.10166, January 25, 2021.
    Published version · arXiv preprint

    Abstract

    The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a self-contained formal and constructive proof of Birkhoff's HSP theorem in Martin-Löf dependent type theory. In the course of our presentation, we highlight some of the more challenging aspects of formalizing the basic definitions and theorems of universal algebra in type theory. Nonetheless, we hope this paper and the agda-algebras library serve as further evidence in support of the claim that dependent type theory and the Agda language, despite the technical demands they place on the user, are accessible to working mathematicians (such as ourselves) who possess sufficient patience and resolve to formally verify their results with a proof assistant. Indeed, the agda-algebras library now includes a substantial collection of definitions, theorems, and proofs from universal algebra, illustrating the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures.

  • Dedekind's Transposition Principle for lattices of equivalence relations
    William DeMeo.
    arXiv preprint arXiv:1301.6788, January 28, 2013.
    arXiv preprint

    Abstract

    We prove a version of Dedekind's Transposition Principle that holds in lattices of equivalence relations.

  • Interval enforceable properties of finite groups
    William DeMeo.
    arXiv preprint arXiv:1205.1927, May 9, 2012.
    arXiv preprint

    Abstract

    We propose a classification of group properties according to whether they can be deduced from the assumption that a group's subgroup lattice contains an interval isomorphic to some lattice. We are able to classify a few group properties as being "interval enforceable" in this sense, and we establish that other properties satisfy a weaker notion of "core-free interval enforceable." We also show that if there exists a group property and its negation that are both core-free interval enforceable, this would settle an important open question in universal algebra.

Theses

  • Congruence lattices of finite algebras
    William J. DeMeo.
    PhD thesis, University of Hawaii at Manoa, 2012.
    arXiv preprint

    Abstract

    An important and long-standing open problem in universal algebra asks whether every finite lattice is isomorphic to the congruence lattice of a finite algebra. Until this problem is resolved, our understanding of finite algebras is incomplete, since, given an arbitrary finite algebra, we cannot say whether there are any restrictions on the shape of its congruence lattice. By a well known result of Palfy and Pudlak, the problem would be solved if we could prove the existence of a finite lattice that is not an interval in the lattice of subgroups of a finite group. Thus the problem of characterizing congruence lattices of finite algebras is closely related to the problem of characterizing intervals in subgroup lattices. In this work, we review a number of methods for finding a finite algebra with a given congruence lattice, including searching for intervals in subgroup lattices. We also consider methods for proving that algebras with a given congruence lattice exist without actually constructing them. By combining these well known methods with a new method we have developed, and with much help from computer software like the UACalc and GAP, we prove that with one possible exception every lattice with at most seven elements is isomorphic to the congruence lattice of a finite algebra. As such, we have identified the unique smallest lattice for which there is no known representation. We examine this exceptional lattice in detail, and prove results that characterize the class of algebras that could possibly represent this lattice. We conclude with what we feel are the most interesting open questions surrounding this problem and discuss possibilities for future work.

Edited volumes

  • Proceedings of Algebras and Lattices in Hawaii 2018 (editor)
    Kira Adaricheva, William DeMeo, and Jennifer Hyndman.
    2018.