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 alphaequivalence, 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 deallocation binders, inspired by previous work of Gabbay, Ghica and Petrişan. I will present the initial setup, defining a notion of alphaequivalence 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 