Complete Lattices and Up-to Techniques

Damien Pous 1, 2
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : 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.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00155308
Contributor : Damien Pous <>
Submitted on : Saturday, September 22, 2007 - 4:37:05 PM
Last modification on : Tuesday, November 20, 2018 - 7:50:03 AM
Long-term archiving on : Friday, November 25, 2016 - 5:40:11 PM

File

LIP-RR2007-30.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Damien Pous. Complete Lattices and Up-to Techniques. 5th Asian Symposium on Programming Languages and Systems, Joxan Jaffar, 2007, Singapore, Singapore. pp.351-366, ⟨10.1007/978-3-540-76637-7_24⟩. ⟨ensl-00155308v2⟩

Share

Metrics

Record views

239

Files downloads

282