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.

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?

By Denis Bredelet -jido at Sun, 2007-04-01 10:42 | login or register to post comments

Nothing

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 .

By Felicia Li Svilling at Mon, 2007-04-02 01:35 | login or register to post comments