Mechanizable proofs about parallel processes
J. M. Cadiou, Jean-Jacques Lévy · 1973
This paper attempts to use formal semantics of a class of parallel processes in order to carry out mechanizable proofs about them. The formalism used is LCF (Logic for Computable Functions, Milner [22]), with slight extensions. The processes we consider communicate by sharing memory, rather than by signals on communication lines. Parallelism is treated as nondeterminism. We state properties such as mutual exclusion of critical sections, absence of deadlocks, determinacy, and we show examples of proofs.