An application of co-inductive types in Coq: Verification of the alternating bit protocol Export

@incollection{gimenez-95, abstract = {We describe an experience concerning the implementation and use of co-inductive types in the proof editor Coq. Co-inductive types are recursive types which, opposite to inductive ones, may be inhabited by infinite objects. In order to illustrate their use in Coq, we describe an axiomatisation of a calculus of broadcasting systems where non-ending processes are represented using infinite objects. This calculus is then used for developing a verification proof of the alternating bit protocol.}, author = {Gim\'{e}nez, Eduardo}, citeulike-article-id = {6074528}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-61780-9_67}, citeulike-linkout-1 = {http://www.springerlink.com/content/p24mk844489l6315}, doi = {10.1007/3-540-61780-9_67}, journal = {Types for Proofs and Programs}, keywords = {coinduction, coq, functional-programming, logic, master-project, recursion, theorem-proving, verification}, pages = {135--152}, posted-at = {2009-11-05 14:02:51}, priority = {2}, title = {An application of co-inductive types in Coq: Verification of the alternating bit protocol}, url = {http://dx.doi.org/10.1007/3-540-61780-9_67}, year = {1996} }

TY - CHAP ID - gimenez-95 L3 - citeulike-article-id:6074528 N2 - We describe an experience concerning the implementation and use of co-inductive types in the proof editor Coq. Co-inductive types are recursive types which, opposite to inductive ones, may be inhabited by infinite objects. In order to illustrate their use in Coq, we describe an axiomatisation of a calculus of broadcasting systems where non-ending processes are represented using infinite objects. This calculus is then used for developing a verification proof of the alternating bit protocol. JF - Types for Proofs and Programs EP - 152 TI - An application of co-inductive types in Coq: Verification of the alternating bit protocol SP - 135 KW - coinduction KW - coq KW - functional-programming KW - logic KW - master-project KW - recursion KW - theorem-proving KW - verification AU - Giménez, Eduardo PY - 1996/// UR - http://dx.doi.org/10.1007/3-540-61780-9_67 ER -