CLL: A Concurrent Language Built from Logical Principles
by Deepak Garg, 2005.
In this report, we use both the Curry-Howard isomorphism and proof-search to design a concurrent programming
language from logical principles.
logic is a first-order intuitionistic linear logic where all right synchronous connectives are restricted to a monad.
Yet another example of using monads to embed effectful computations into a pure FP. Another interesting part is the methodology of derivation of a PL from a logic.