Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Broadcast Psi-calculi

view this post on Zulip Email Gateway (Apr 02 2024 at 14:06):

From: Dmitriy Traytel <traytel@di.ku.dk>
A new entry constituting a significant extension of Jesper Bengtson’s good old Psi_Calculi entry with new primitives for broadcasting.

Broadcast Psi-calculi
by Palle Raabjerg, Johannes Åman Pohjola, and Tjark Weber

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.

Enjoy!

view this post on Zulip Email Gateway (Apr 02 2024 at 15:43):

From: Dmitriy Traytel <traytel@di.ku.dk>
And here is the link: https://www.isa-afp.org/entries/Broadcast_Psi.html

(Apologies.)

Last updated: Jan 04 2025 at 20:18 UTC