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.

@unpublished{bsp19,
    title = "Bracket Algebra, a nominal theory of interleaved scopes",
    author = "{Paul Brunet}, {Alexandra Silva}, {Daniela Petrişan}",
    year = 2019,
}

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