Type Directed Concurrency

Type Directed Concurrency by Deepak Garg and Frank Pfenning (2005)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concurrent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their different computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus.

This paper doesn't seem to even have been mentioned on LtU before. Frank Pfenning is one of the computer scientists I watch and this is related to LolliMon and CLF which I find quite interesting. The language that results is very LolliMon/CLF-esque.

Comment viewing options

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

Minimal concurrency

Since the functional and the concurrent sublanguages are orthogonal, we can ask: what is the smallest set of constructs that introduce concurrency?

I am just talking about making use of multiple processors, not (yet) message-passing or shared state. I suppose we need link, since it bridges the concurrent world with the functional one. Then conjonction? What else?


If you just want to make use of multiple processors, you dont have to add anything to a pure functional language. Look at Data Parallel Haskell .

Type directed concurrency...

Type directed concurrency... That sounds like a great program.

I understand that is explicit parallelism right? I find the notation in the paper rather obscure and hard to follow.