Linear Resources and Process Compositions (Q7361535)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry ProcessComposition
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Linear Resources and Process Compositions |
AFP entry ProcessComposition |
Statements
25 November 2024
0 references
Filip Smola
0 references
Jacques D. Fleuriot
0 references
Linear Resources and Process Compositions (English)
0 references
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.
0 references
