• Maribel Fernández (Kings College London)

Title: Nominal Syntax with Atom Substitutions

Abstract: Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: Nominal syntax is a generalisation of first-order syntax that includes names, a notion of name binding and an elegant axiomatisation of alpha-equivalence, based on nominal set theory. However, it does not take into account non-capturing atom substitution, which is not a primitive notion in nominal syntax.

We consider an extension of nominal syntax with non-capturing atom substitutions and show that matching is decidable and finitary but unification is undecidable in general. The proof of undecidability of unification is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms.

We provide a general matching algorithm and characterise a class of problems for which matching is unitary, giving rise to expressive and efficient notions of rewriting.

This is joint work with Jesus Dominguez.

• Alexandra Silva (University College London)

Title: An algebraic framework to reason about concurrency

Abstract: Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency.

The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi. Detailed references can be found on the CoNeCo project website: https://coneco-project.org/.