Bracket Algebra, a nominal theory of interleaved scopes

with Alexandra Silva and Daniela Petrişan .

technical report, 2019

In this paper we present bracket algebra, a nominal framework that can be used in reasoning about programs with interleaved scopes. We construct a hierarchy of languages based on their memory and binding power. We present a decision procedure for program equivalence and containment for a large class of programs.

Links

Draft

Other ressources

Coq proof on Github

Related talks
	A Kleene Theorem for Nominal Automata ICALP in Patras, July 2019 .	More
	Bracket Algebra Highlights in Berlin, September 2018 .	More
	A formal exploration of Nominal Kleene Algebra MFCS in Krakow, August 2016 .	More
Related papers
	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