An equational theory for weak bisimulation via generalized parameterized coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
Abstract
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.
Topics & Concepts
CoinductionBisimulationMathematical proofContext (archaeology)Parameterized complexityMathematicsComputer scienceEquational logicAlgebra over a fieldMathematical logicCalculus (dental)Discrete mathematicsTheoretical computer scienceClass (philosophy)ConcurrencyAbstractionLogic, programming, and type systemsLogic, Reasoning, and KnowledgeFormal Methods in Verification