A lean mechanization of reversible occurrence nets

DOI10.1007/978-3-032-30839-9_5MaRDI QIDQ7411923zbMATH OpenFDO

Authors Daniel Dávalos, Hernan Melgratti

Publication date 2026

Full work available at URL https://doi.org/10.1007/978-3-032-30839-9_5

zbMATH Keywords

concurrencyproof mechanizationreversibility

Mathematics Subject Classification ID

Other nonclassical models of computation (68Q09) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68)

Cites work

• A certified study of a reversible programming language
• A collective interpretation semantics for reversing Petri nets
• A reversible perspective on Petri nets and event structures
• A truly concurrent semantics for reversible CCS
• An axiomatic theory for reversible computation
• Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean}
• Checkpoint/rollback vs causally-consistent reversibility
• En garde! Unguarded iteration for reversible computation in the delay monad
• Petri nets, event structures and domains. I
• Reversible computation in nets with bonds
• Reversible occurrence nets and causal reversible prime event structures
• Reversing place transition nets
• Sequential and concurrent behaviour in Petri net theory
• Taming confusion for modeling and implementing probabilistic concurrent systems
• The Lean 4 theorem prover and programming language
• The non-sequential behaviour of Petri nets

This page was built for publication: A lean mechanization of reversible occurrence nets

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