Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
From MaRDI portal
Publication:5327356
DOI10.1007/978-3-642-39634-2_26zbMath1317.68209OpenAlexW165755327MaRDI QIDQ5327356
Martin Bodin, Jörg Endrullis, Dimitri Hendriks
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_26
Related Items (7)
Unnamed Item ⋮ A Mechanized Theory of Regular Trees in Dependent Type Theory ⋮ Proving language inclusion and equivalence by coinduction ⋮ Enhanced coalgebraic bisimulation ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ Companions, Codensity and Causality ⋮ Unnamed Item
Uses Software
This page was built for publication: Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
