Nondeterministic asynchronous dataflow in Isabelle/HOL

DOI10.4230/LIPICS.ITP.2025.30MaRDI QIDQ7323687zbMATH OpenFDO

Authors Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.30

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A fully abstract trace model for dataflow and asynchronous networks
• Code generation via higher-order rewrite systems
• Data refinement in Isabelle/HOL
• Friends with benefits. Implementing corecursion in foundational proof assistants
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 7730622 (Why is no real title available?)
• scientific article; zbMATH DE number 7699427 (Why is no real title available?)
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Network algebra for asynchronous dataflow^∗
• New up-to techniques for weak bisimulation
• Process algebra for synchronous communication
• The algebra of stream processing functions
• Truly modular (co)datatypes for Isabelle/HOL
• Weak Bisimulation Up to Elaboration

This page was built for publication: Nondeterministic asynchronous dataflow in Isabelle/HOL

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