Damien Pous

LPAR Conference 2018 Conference Paper

Left-Handed Completeness for Kleene algebra, via Cyclic Proofs

• Anupam Das 0002
• Amina Doumane
• Damien Pous

We give a new proof that the axioms of left-handed Kleene algebra are complete with respect to language containments. This proof is significantly simpler than both the proof of Boffa (which relies on Krob’s completeness result), and the more recent proof of Kozen and Silva. Our proof builds on a recent non-wellfounded sequent calculus which makes it possible to explicitly compute the invariants required for left-handed Kleene algebra.

CSL Conference 2018 Conference Paper

Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)

• Anupam Das 0002
• Damien Pous

We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.

MFCS Conference 2018 Conference Paper

Treewidth-Two Graphs as a Free Algebra

• Christian Doczkal
• Damien Pous

We give a new and elementary proof that the graphs of treewidth at most two can be seen as a free algebra. This result was originally established through an elaborate analysis of the structure of K_4-free graphs, ultimately reproving the well-known fact that the graphs of treewidth at most two are precisely those excluding K_4 as a minor. Our new proof is based on a confluent and terminating rewriting system for term-labeled graphs and does not involve graph minors anymore. The new strategy is simpler and robust in the sense that it can be adapted to subclasses of treewidth-two graphs, e. g. , graphs without self-loops.

Highlights Conference 2017 Conference Abstract

Coinduction up to and automata algorithms

• Damien Pous

Highlights Conference 2017 Conference Abstract

Coinduction up to and automata algorithms

• Damien Pous

MFCS Conference 2017 Conference Paper

K4-free Graphs as a Free Algebra

• Enric Cosme-Llópez
• Damien Pous

Graphs of treewidth at most two are the ones excluding the clique with four vertices as a minor. Equivalently, they are the graphs whose biconnected components are series-parallel. We turn those graphs into a free algebra, answering positively a question by Courcelle and Engelfriet, in the case of treewidth two. First we propose a syntax for denoting them: in addition to series and parallel compositions, it suffices to consider the neutral elements of those operations and a unary transpose operation. Then we give a finite equational presentation and we prove it complete: two terms from the syntax are congruent if and only if they denote the same graph.

MFCS Conference 2016 Conference Paper

A Formal Exploration of Nominal Kleene Algebra

• Paul Brunet
• Damien Pous

An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent. Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i. e. , atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more expressive remains open. All our results were formally checked using the Coq proof assistant.

CSL Conference 2010 Conference Paper

Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

• Damien Pous

Abstract We prove ”untyping” theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped equations. As a consequence, the corresponding untyped decision procedures can be extended for free to the typed settings. Some of these theorems are obtained via a detour through fragments of cyclic linear logic, and give rise to a substantial optimisation of standard proof search algorithms.

TCS Journal 2008 Journal Article

Using bisimulation proof techniques for the analysis of distributed abstract machines

• Damien Pous

We illustrate the use of recently developed proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. We first define this framework, and then focus on the algorithm which is used to route messages asynchronously to their destination. A first version of this algorithm can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.

TCS Journal 2007 Journal Article

New up-to techniques for weak bisimulation

• Damien Pous

Up-to techniques have been introduced to enhance the bisimulation proof method for establishing bisimilarity results. While up-to techniques for strong bisimilarity are well understood, the irregularities that appear in the weak case make it difficult to give a unified presentation. We propose a uniform and modular theory of up-to techniques for weak bisimulation that captures most of the existing proof technology and introduces new techniques. Some proofs rely on nontrivial–and new–commutation results based on termination guarantees. All results presented in this paper have been formally proved using the Coq proof assistant.