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

DOI10.1007/3-540-61780-9_67zbMath1407.68435OpenAlexW1480957705MaRDI QIDQ4647576

No author found.

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

Related Items (3)

Squeezing streams and composition of self-stabilizing algorithms ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ A Prospectus for Mobile Broadcasting Systems

Uses Software

• Coq
• ALF

Cites Work

• Automating inversion of inductive predicates in Coq
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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