English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Coinductive reasoning about infinitary structures such as streams is widelyapplicable. However, practical frameworks for developing coinductive proofs andfinding reasoning principles that help structure such proofs remain achallenge, especially in the context of machine-checked formalization.  This paper gives a novel presentation of an equational theory for reasoningabout structures up to weak bisimulation. The theory is both compositional,making it suitable for defining general-purpose lemmas, and also incremental,meaning that the bisimulation can be created interactively. To prove thetheory's soundness, this paper also introduces generalized parameterizedcoinduction, which addresses expressivity problems of earlier works andprovides a practical framework for coinductive reasoning. The paper presentsthe resulting equational theory for streams, but the technique applies to otherstructures too.  All of the results in this paper have been proved in Coq, and the generalizedparameterized coinduction framework is available as a Coq library.

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction