Sanjiv Ranchod: Category Theoretic Models of Substitution for Substructural Theories

Abstract

In [1], Fiore, Plotkin and Turi introduce category theoretic models, in the setting of first-order cartesian theories, of single-variable substitution as substitution algebras and simultaneous substitution as substitution monoids to model the abstract syntax of binding signatures. Various authors have since considered substitution monoids and binding signatures in the substructural settings of linear and affine theories. More recently, the underlying substitution monoidal structures have been extended to cartesian closed bicategories. In this talk, we recast the construction of a substitution algebra for cartesian theories, which allows it to be extended to the linear, affine and relevant settings, and uniformly develop the abstract syntax for binding signatures [2]. Following a review of the literature on substitution monoids, we generalise to a theory encompassing cartesian, linear, affine and relevant sorts together with substructural coercions, and similarly extend this construction to a bicategory [3]. Joint work with Marcelo Fiore.

[1] M. Fiore, G. Plotkin and D. Turi, Abstract syntax and variable binding (extended abstract), 14th Symposium on Logic in Computer Science (1999), 193–202.
[2] M. Fiore, S. Ranchod, Substructural Abstract Syntax with Variable Bindingand Single-Variable Substitution, 40th Symposium on Logic in Computer Science (2025), to appear.
[3] M. Fiore, S. Ranchod, Substitution for Substructural Theories, in preparation.