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

DOI10.1007/3-540-61780-9_67zbMATH Open1407.68435OpenAlexW1480957705MaRDI QIDQ4647576FDOQ4647576

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

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

zbMATH Keywords

elimination ruletransition relationinductive typerecursive callbroadcasting system

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Squeezing streams and composition of self-stabilizing algorithms
• \(\pi\)-calculus in (Co)inductive-type theory
• A bitopological view on cocompact extensions

Uses Software

• Coq
• ALF

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)