Complete Lattices and Up-to Techniques

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.
Type de document :
Communication dans un congrès
Zhong Shao. 5th Asian Symposium on Programming Languages and Systems, Singapore, Singapore. Springer Berlin / Heidelberg, pp.351-366, 2007, volume 4807 of Lecture Notes in Computer Science. 〈10.1007/978-3-540-76637-7_24〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00155308
Contributeur : Damien Pous <>
Soumis le : samedi 22 septembre 2007 - 16:37:05
Dernière modification le : mardi 24 avril 2018 - 13:52:27
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 17:40:11

Fichier

LIP-RR2007-30.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Damien Pous. Complete Lattices and Up-to Techniques. Zhong Shao. 5th Asian Symposium on Programming Languages and Systems, Singapore, Singapore. Springer Berlin / Heidelberg, pp.351-366, 2007, volume 4807 of Lecture Notes in Computer Science. 〈10.1007/978-3-540-76637-7_24〉. 〈ensl-00155308v2〉

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

137