Home

CLL: A Concurrent Language Built from Logical Principles

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. ... Our underlying 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.
By Andris Birkmanis at 2007-06-30 18:06 | Logic/Declarative | Semantics | Type Theory | other blogs | 12736 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

A simpler version

...of the paper with less details and smaller language: Type-Directed Concurrency.

In this paper we show that the two views of computation, via proof reduction and via proof search, are not inherently incompatible, but can coexist harmoniously in a language that combines functional and concurrent computation. We retain the strong guarantees for functional computation without unduly restricting the dynamism of concurrent computation.

In order to achieve this synthesis, we employ several advanced building blocks.

The first is linearity: as has been observed, the evolution and communication of processes maps naturally to the single-use semantics of assumptions in linear logic.

The second is dependency: we use dependent types to model com-
munication channels and also to retain the precision of functional specifications for transmitted values.

The third is monads: we use monadic types to encapsulate concurrent computation, so that the linear connectives can retain the same logical meaning on the functional and concurrent side without interference.

The fourth is focusing: we use it to enforce the atomicity of concurrent interactions during proof search.

For some reason this approach seemed familiar, and now I know why.

By Andris Birkmanis at Sat, 2007-06-30 19:29 | login or register to post comments

Nice paper

Where's the code?

By taral at Wed, 2007-07-04 22:25 | login or register to post comments