Diacritical Companions

Abstract : Coinductive reasoning in terms of bisimulations is in practice routinely supported by carefully crafted up-to techniques that can greatly simplify proofs. However, designing and proving such bisimulation enhancements sound can be challenging, especially when striving for modularity. In this article, we present a theory of up-to techniques that builds on the notion of companion introduced by Pous and that extends our previous work which allows for powerful up-to techniques defined in terms of diacritical progress of relations. The theory of diacritical companion that we put forward works in any complete lattice and makes it possible to modularly prove soundness of up-to techniques which rely on the distinction between passive and active progresses, such as up to context in λ-calculi with control operators and extensionality.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, May 21, 2019 - 4:49:00 PM
Last modification on : Wednesday, May 22, 2019 - 1:32:16 AM


Files produced by the author(s)


  • HAL Id : hal-02136002, version 1



Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Diacritical Companions. Mathematical Foundations of Programming Semantics, Jun 2019, London, United Kingdom. ⟨hal-02136002⟩



Record views


Files downloads