A Complete Axiomatisation of a Fragment of Language Algebra

conference paper, in CSL 2020

We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.

Links

	Permanent link
	Preprint on HAL
	Paper on DROPS - LIPIcs

Other ressources

Coq proof on Github

Related talks
	A complete axiomatisation of a fragment of language algebra CSL in Barcelona, January 2020 .	More
	The theory of languages Highlights in London, September 2017 .	More
	The Equational Theory of Algebras of Languages BLAST in Nashville, August 2017 .	More
	The Equational Theory of Algebras of Languages RAMiCS in Lyon, May 2017 (Special session on mechanised reasoning) .	More
	The Equational Theory of Algebras of Languages PPLV Seminar in London, April 2017 .	More
Related papers
	Reversible Kleene lattices (in MFCS 2017)	More