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

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.