The "propagator" paper would be more interesting if there was a use case in the paper. The basic idea is to have a graph of computational elements, but insist that the elements be commutative, associative, and idempotent. Under those restrictions, you get the same answer despite race conditions, which leads to a simple model of asynchronous programming. But what is this good for? I could sort of see a theorem prover that works like this. Beyond logic problems, it's harder to find an application.
This might be a good way to implement consistent-eventually systems. Those are hard to get right, and having to build them out of elements which have the propagator components might help. Not sure this is possible, but it's worth a try if you have to solve that problem.