  The need for rigorous process composition is encountered in many situations
pertaining to the development and analysis of complex systems. We discuss the
use of Classical Linear Logic (CLL) for correct-by-construction resource-based
process composition. Abstract processes are specified as CLL sequents
describing the types of input and output resources. The proofs-as-processes
paradigm and its recent evolutions enable the composition of such processes via
logical inference, with mathematical guarantees when it comes to concurrent
execution, deadlock freedom, and systematic resource accounting. We introduce
algorithms to automate the necessary inference steps for binary compositions of
processes in parallel, conditionally, and in sequence. We combine decision
procedures and heuristics to achieve intuitive and practically useful
compositions in an applied setting. Our work is implemented within the formal
setting of the HOL Light proof assistant and incorporated in the WorkflowFM
prototype to facilitate diagrammatic, correct-by-construction process
workflows.

Logic in Computer Science