Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Tuesday, May 21, 2019 - 4:49:00 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:48 AM


Files produced by the author(s)




Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Diacritical Companions. MFPS 2019-Mathematical Foundations of Programming Semantics XXXV, Jun 2019, London, United Kingdom. ⟨10.1016/j.entcs.2019.09.003⟩. ⟨hal-02136002⟩



Les métriques sont temporairement indisponibles