Rencontre, June 25, 2026

Programme

• Francesco Gavazzo (Università di Padova, It)
  Invited talk: Term Relation Algebras and the Algebraization of Language Metatheory

  Many semantic aspects of a formal language can be defined as structural predicates on its abstract syntax, and much of its metatheory can be understood through the 'logical' properties of these predicates. Typical examples include results such as congruence of bisimilarity, type safety, confluence of evaluation, and termination of reduction. While several general theories have been proposed to study some of these properties — notable examples include mathematical operational semantics and categorical rewriting — a theory accounting for all of them, uniformly and abstractly, independently of specific languages and syntactic structures, is still missing.

  In a recent line of research, I have proposed to develop such a theory in the form of an algebra of structural predicates, extending traditional logical algebras with operations akin to the structural definitions of predicates, such as structural recursion and substitution. This talk gives an introduction to such algebras in their relational form — Term Relation Algebras (TRAs) — and to their applications to the metatheory of programming languages and formal systems.

  The first part of the talk introduces TRAs from an 'algebraic logic' perspective. TRAs arise as algebras of relations on term structures, internalizing such structure through logical operations on relations. Remarkably, not only is this 'logical internalization' possible on virtually all term structures — first- and second-order terms, nominal terms, string diagrams, and so on — but it yields, in all these cases, essentially the same algebras. TRAs axiomatize these algebras abstractly, with no reference to any underlying term structure.

  The second part shifts to applications of TRAs to language metatheory, showing how many of the semantic notions and properties mentioned above can be studied algebraically within TRAs. The payoff of the algebraization is generality and unification: on the one hand, metatheorems that are otherwise reproved system by system are proved once and for all as algebraic properties (mostly quasi-equations) in the framework of TRAs; on the other hand, the algebraic lens reveals how conceptually different metatheorems, such as confluence of reduction and congruence of bisimilarity, are actually deeply related. 

  Time permitting, the last part of the talk is devoted to some informal comparisons between TRAs and 'proof-theoretic' approaches to language metatheory.

  • June 25, 2026, 10:30 a.m.
• Adrienne Lancelot (Università di Bologna, IT)
  Invited talk: A Simple Formal Proof of the Genericity Lemma

  Barendregt's genericity lemma (1984) is a classic result in the theory of the λ-calculus, formalizing the fact that meaningless terms are sort of black holes for evaluation: if evaluation should ever enter them, it would never get out. Ten years later, in 1994, Takahashi publishes a two-page paper titled "A Simple Proof of the Genericity Lemma". Many other proof developments now exist, including an 8-line proof using Taylor Expansion (Barbarossa-Manzonetto 2020) and genericity lemmas for call-by-value evaluation (Accattoli-Lancelot 2024; Arrial-Guerrieri-Kesner 2024; ...).

  In this talk, I will explain why genericity is a cornerstone result in Barendregt's book and why I think it is still relevant today (in particular viewed as a result on program preorders). I will overview the different possible proof techniques and tell you about our formalization in the Abella proof assistant of Takahashi's technique: a two-page paper turns into roughly 2500 lines of code.

  The end of the talk will hopefully mention open questions and future work on the topic.

  Based on: Light Genericity, FoSSaCS 2024 https://link.springer.com/chapter/10.1007/978-3-031-57231-9_2; Barendregt's Theory of the λ-calculus, Refreshed and Formalized, ITP 2025 https://doi.org/10.4230/LIPIcs.ITP.2025.13; and my PhD thesis, 2025 https://theses.hal.science/tel-05407883

• Niccolò Veltri (Tallinn University of Technology, ES)
  Invited talk: Semi-Associative Substructural Logics

  Substructural logics are logical systems lacking one or more structural rules among exchange, weakening and contraction. Notable instances of substructural logics include Girard's linear logic and its non-commutative variants, among which prominently figures the syntactic calculus of Lambek. Motivated by application in linguistics, proof-theorists have also studied logics lacking more primitive structural rules, such as associativity.

  In this talk, I will introduce semi-associative substructural logics, which are logical systems allowing only a restricted, directed version of associativity. The motivation for studying these logics come from their categorical models, which are Street's skew monoidal closed categories. I will present a cut-free sequent calculus, presenting the free skew monoidal closed category on a set of atomic formulae. Then I will discuss some proof-theoretic results: proof normalization, extensions with additive connectives and, time permitting, Craig interpolation.