Diacritical Companions - Archive ouverte HAL Access content directly
Conference Papers Year :

Diacritical Companions

(1) , (2) , (1)


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.
Fichier principal
Vignette du fichier
companion.pdf (367.06 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02136002 , version 1 (21-05-2019)



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⟩
239 View
109 Download



Gmail Facebook Twitter LinkedIn More