An equational theory for weak bisimulation via generalized parameterized coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic · 2020
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization.