Paper: An Algebraic Approach to Formal System Metatheory (at LICS 2026)

Authors: Francesco Gavazzo

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.50

Abstract

We introduce an algebraic approach to the metatheory of formal systems of term assertions akin to those of structural and natural operational semantics, type theories, rewriting systems, and equational theories. We rest on Term Relation Algebras, viz. pointfree algebras of structurally-defined predicates on terms, to give a common algebraic semantics to different kinds of formal systems, regardless of their inferential mechanisms and underlying term structures. This enables abstract reasoning about formal systems, and their metatheory, through the algebra of the term predicates they define. We give a faithfully term-free algebraization of semantically-relevant term predicates, such as parallel reduction, big-step evaluation, and applicative bisimilarity. We extend this algebraization also to fundamental metatheoretical properties of these notions - including congruence of applicative bisimilarity, determinacy of evaluation, and confluence of reduction - and prove these properties using algebraic methods.

BibTeX

  @InProceedings{Gavazzo-AnAlgebraicApproach,
    author = 	 {Francesco Gavazzo},
    title = 	 {An Algebraic Approach to Formal System Metatheory},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {50:1--50:31},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.50}
  }