Bracket Algebra

Highlights in Berlin, September 2018

Nominal techniques have received a lot of attention in recent years, as they describe in a simple yet precise manner phenomena related to variable renaming, like alpha-equivalence, scopes, locality... However, they seem to suffer from two shortcomings: they are not yet able to handle interleaved scopes, and do not apply well to relational semantics of programs. In this talk I will describe an ongoing project to provide an algebraic treatment of the semantics of programming languages which contain explicitly allocation and de-allocation binders, inspired by previous work of Gabbay, Ghica and Petrişan. I will present the initial setup, defining a notion of alpha-equivalence of traces, and briefly describe how this may be extended to regular languages. I will present some decidability results we obtained, and hint at future investigations. Most of these developments have been formalised in Coq. This is joint work with Alexandra Silva and Daniela Petrisan.

Related talks
	A Kleene Theorem for Nominal Automata ICALP in Patras, July 2019 .	More
	A formal exploration of Nominal Kleene Algebra MFCS in Krakow, August 2016 .	More
Related papers
	Bracket Algebra, a nominal theory of interleaved scopes (2019) with Alexandra Silva and Daniela Petrişan.	More
	A Kleene theorem for nominal automata (in ICALP 2019) with Alexandra Silva.	More
	Algebras of relations: from algorithms to formal proofs (in Université de Lyon 2016)	More
	A formal exploration of nominal Kleene algebra (in MFCS 2016) with Damien Pous.	More