Damien Pous' Home Page.

A COQ Formalisation of Up-to Techniques for Weak Bisimulation

In 2005, we proposed a theory for up-to techniques for bisimilarity, in this paper, that appeared in the proceedings of ICALP'05. An extended version appeared in TCS since; slides for ICALP05 are available here (printable version).

Abstract (05): 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, in the weak case they come as a collection of unrelated results, and lack a unified presentation.
We propose a uniform and modular theory of up-to techniques for weak bisimulation that captures existing proof technology and introduces new techniques. Some proofs rely on non trivial -- and new -- commutation results based on termination guarantees.
The flexibility and usefulness of our framework is illustrated on two examples, one of them coming from a recent study of a distributed abstract machine.

All the results of the first paper have been formalised and checked using the COQ Proof Assistant. Here are the COQ sources (under GPL). Here is the coqdoc generated documentation (the numbering of results corresponds to the published - short - paper). The developments are structured as follows:

In 2006, we extended this work in this CONCUR paper. Here are a long version, with full proofs, the slides, and printable slides.

Abstract (06): We study the use of the elaboration preorder (due to Arun-Kumar and Natarajan) in the framework of up-to techniques for weak bisimulation. We show that elaboration yields a correct technique that encompasses the commonly used up to expansion technique. We also define a theory of up-to techniques for elaboration that in particular validates an elaboration up to elaboration technique, while it is known that weak bisimulation up to weak bisimilarity is unsound. In this sense, the resulting setting improves over previous works in terms of modularity.
Our results are obtained using nontrivial proofs that exploit termination arguments. In particular, we need the termination of internal computations for the up-to techniques to be correct. We show how this condition can be relaxed to some extent in order to handle processes exhibiting infinite internal behaviour.

In 2007, we defined a more general theory of up-to techniques for coinduction (presented at APLAS; here are the slides and printable slides).

Abstract (07): We propose a theory of up-to techniques for proofs by coinduction, in the setting of complete lattices. This theory improves over existing results by providing a way to compose arbitrarily complex techniques with standard techniques, expressed using a very simple and modular semi-commutation property.
Complete lattices are enriched with monoid operations, so that we can recover standard results about labelled transitions systems and their associated behavioural equivalences at an abstract, ``point-free'' level.
Our theory gives for free a powerful method for validating up-to techniques. We use it to revisit up to contexts techniques, which are known to be difficult in the weak case: we show that it is sufficient to check basic conditions about each operator of the language, and then rely on an iteration technique to deduce general results for all contexts.

The last paper, together with other results to appear in my PhD dissertation, make it possible to formalise all of these results in a simpler and nicer way. I'm currently workink on this.