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.

Additional Metadata
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)
Publisher Springer
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
Citation
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.