An application of co-inductive types in Coq: Verification of the alternating bit protocol
- 1 January 1996
- book chapter
- Published by Springer Nature
- p. 135-152
- https://doi.org/10.1007/3-540-61780-9_67
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- Automating inversion of inductive predicates in CoqPublished by Springer Nature ,1996
- A calculus of broadcasting systemsScience of Computer Programming, 1995
- The Alf proof editor and its proof enginePublished by Springer Nature ,1994
- Proof-checking a data link protocolPublished by Springer Nature ,1994
- Infinite objects in type theoryPublished by Springer Nature ,1994
- IsabellePublished by Springer Nature ,1994
- Programming with broadcastsPublished by Springer Nature ,1993