Abstract
In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.
We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.
License
Topics
Related publications
- Smola, F., & Fleuriot, J. D. (2024). Linear Resources in Isabelle/HOL. Journal of Automated Reasoning, 68(2). https://doi.org/10.1007/s10817-024-09698-2
Session ProcessComposition
- Util
- ResTerm
- ResNormalForm
- ResNormRewrite
- ResNormDirect
- ResNormCompare
- Resource
- Process
- CopyableElimination