Diacritical companions

D Biernacki, S Lenglet, P Polesiuk - Electronic Notes in Theoretical …, 2019 - Elsevier
D Biernacki, S Lenglet, P Polesiuk
Electronic Notes in Theoretical Computer Science, 2019Elsevier
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 …
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.
Elsevier