2009
Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme
Publication
Publication
Presented at the
International Conference Types for Proofs and Programs, Torino, Italy
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 | |
|---|---|
| , | |
| Springer | |
| S. Berardi , F. Damiani , U. de'Liguoro | |
| Lecture Notes in Computer Science | |
| Mending the Unending: Machine Assisted Reasoning with Infinite Objects | |
| International Conference Types for Proofs and Programs | |
| Organisation | Computer Security |
|
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. |
|