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 ed 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: Conference
• Year: 2007
• Where: APLAS
• Authors: Damien Pous
• Keywords: APLAS 2007, Complete Lattices, Programming Languages, Standard Techniques, Up-to Techniques