Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme
In this work we present a modular theory of the coalgebras and bisimulation in the intensional type theory implemented in Coq. On top of that we build the theory of weakly final coalgebras and develop the $\lambda$-coiteration scheme, thereby extending the class of specifications definable in Coq. We provide an instantiation of the theory for the coalgebra of streams and show how some of the productive specifications violating the guardedness condition of Coq can be formalised using our library.
|Keywords||Coinduction - Coalgebra - Bisimulation - Coiteration - Coq|
|ACM||Mathematical Logic (acm F.4.1), Deduction and Theorem Proving (acm I.2.3)|
|MSC||Theorem proving (deduction, resolution, etc.) (msc 68T15)|
|THEME||Software (theme 1)|
|Editor||S. Berardi , F. Damiani , U. de'Liguoro|
|Series||Lecture Notes in Computer Science|
|Project||Mending the Unending: Machine Assisted Reasoning with Infinite Objects|
|Conference||International Conference Types for Proofs and Programs|
Niqui, M. (2009). Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme. In S Berardi, F Damiani, & U de'Liguoro (Eds.), Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008. Revised Selected Papers (pp. 272–288). Springer.