DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.10

Equational Reasoning in Languages with Binders via Permutation Fixed-Points

Authors: Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

Equational reasoning with binders and structural congruence is difficult due to the interaction between name binding and algebraic laws. Equational theories such as commutativity induce forms of permutation invariance on names that are not captured by standard approaches to the formalisation of syntax with binders. We show that in the nominal setting, this limitation can be addressed by using generalised permutation fixed-point constraints to make invariance explicit. This yields a uniform framework for reasoning about equality of nominal terms modulo α-equivalence and arbitrary equational theories. We introduce a proof system and show that it is sound and complete with respect to a nominal-set semantics, which explains how symmetry can be internalised via fixed-point constraints viewed as N-quantified stabiliser conditions. We provide examples in Milner’s π-calculus - a well-known model of concurrent computation that includes binders and non-trivial structural congruences.

Cite as

Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, and Daniele Nantes-Sobrinho. Equational Reasoning in Languages with Binders via Permutation Fixed-Points. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cairessantos_et_al:LIPIcs.FSCD.2026.10,
  author =	{Caires-Santos, Ali K. and Fern\'{a}ndez, Maribel and Gabbay, Murdoch James and Nantes-Sobrinho, Daniele},
  title =	{{Equational Reasoning in Languages with Binders via Permutation Fixed-Points}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.10},
  URN =		{urn:nbn:de:0030-drops-263609},
  doi =		{10.4230/LIPIcs.FSCD.2026.10},
  annote =	{Keywords: Binding, alpha-equivalence, nominal algebra, permutation fixed-point}
}

Search Results

Documents authored by Gabbay, Murdoch James

Equational Reasoning in Languages with Binders via Permutation Fixed-Points

Abstract

Cite as

Thanks for your feedback!

Could not send message