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

DOI10.1007/3-540-61780-9_67MaRDI QIDQ4647576zbMATH OpenOpenAlexFDO

Authors

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61780-9_67

zbMATH Keywords

elimination ruletransition relationinductive typerecursive callbroadcasting system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formalizing process algebraic verifications in the calculus of constructions
• Certifying circuits in type theory
• scientific article; zbMATH DE number 683368
• Circular coinduction in Coq using bisimulation-up-to techniques
• scientific article; zbMATH DE number 3958712

Cites work

• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 3557754 (Why is no real title available?)
• scientific article; zbMATH DE number 3566181 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• Automating inversion of inductive predicates in Coq

Cited in

(6)

• From Sets to Bits in Coq
• Verification of redecoration for infinite triangular matrices using coinduction
• A prospectus for mobile broadcasting systems
• -calculus in (Co)inductive-type theory
• Squeezing streams and composition of self-stabilizing algorithms
• A bitopological view on cocompact extensions

Describes a project that uses

Uses Software

• ALF
• Coq

This page was built for publication: An application of co-inductive types in Coq: verification of the alternating bit protocol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647576)