Avoiding Spurious Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework
Ruy Ley-Wild, Frank Pfenning · 2010
The Concurrent Logic Framework (CLF) is a foundational type theory for encoding concurrent computations by representing resources with linearity and encapsulating the effects of concurrency in a monad. The definition of concurrent equality via commuting conversions identifies computations differing only in the order of execution of independent steps, capturing a form of true concurrency in a proof-theoretic way. However, some examples suffer from spurious dependencies whereby independent computations cannot be reordered because they use the same shared resource but are not causally linked, or computations are distinguished even though they only differ in the use of isomorphic objects. We address these limitations by incorporating a linear proof irrelevance modality and adopting a richer definition of equality that admits reordering computations modulo proof irrelevant terms. We present several encodings of stateful concurrent systems to demonstrate the usefulness of this extension.