Broadcast Psi-calculi

Palle Raabjerg, Johannes Åman Pohjola, and Tjark Weber. Archive of Formal Proofs, March 2024. Formal proof development.

Abstract

We provide an Isabelle/HOL-Nominal formalisation of the definitions, theorems and proofs in the paper Broadcast Psi-calculi with an Application to Wireless Protocols by Borgström et al., which extends the Psi-calculi framework with primitives for broadcast communication in order to model wireless protocols.

Download

The original publication is available at https://www.isa-afp.org/entries/Broadcast_Psi.html.

BibTeX

@article{raabjerg24broadcast,
  author   = {Palle Raabjerg and Johannes {\AA}man Pohjola and Tjark Weber},
  title    = {Broadcast {Psi}-calculi},
  journal  = {Archive of Formal Proofs},
  month    = mar,
  year     = {2024},
  note     = {\url{https://www.isa-afp.org/entries/Broadcast_Psi.html}, Formal proof development}
}