9
$\begingroup$

In Girard's Proofs and Types we can read :

From an algorithmic viewpoint, the sequent calculus has no Curry-Howard isomorphism, because of the multitude of ways of writing the same proof. This prevents us from using it as a typed $\lambda$-calculus, although we glimpse some deep structure of this kind, probably linked with parallelism.

Proofs and Types, J.Y Girard (Page 28)

But we can also read (about Linear Logic) that

From the viewpoint of computer science, it gives a new approach to questions of laziness, side effects and memory allocation [GirLaf, Laf87, Laf88] with promising applications to parallelism.

Proofs and Types, J.Y Girard (Page 149, written by Yves Lafont)

How are parallel programs linked to the Curry-Howard isomorphism ? What are the current thoughts about that ?

$\endgroup$
7
$\begingroup$

The Concurrent Logical Framework is one interesting area including its descendants, like Linear Meld and LolliMon. This is based on intuitionistic linear logic.

Classical linear logic has connections to the Linear Chemical Abstract Machine (CHAM) as described by e.g. A Calculus for Interaction Nets Based on the Linear Chemical Abstract Machine which explicitly describes the result as a Curry-Howard type result.

Alexander Summers' thesis Curry-Howard Term Calculi for Gentzen-Style Classical Logics which I have not read seems to be aimed directly at the problem of providing a Curry-Howard correspondence for Gentzen-style calculi. The $\lambda\mu$-calculus by Curien and Herbelin introduced in The Duality of Computation is a seminal work in this vein of (non-linear) lambda calculi corresponding to classical logics.

At any rate, this is all still a lively area of research. There are many recent papers on this topic. The above doesn't even mention the even more substructural side of separation logic and the corresponding Hoare Type Theory which focuses on imperative programming languages. For example, there's Towards type-theoretic semantics for transactional concurrency whose references you can trace for prior work.

(As a bit of a pedantic note, most of these are focused on concurrency, not parallelism per se.)

$\endgroup$
  • $\begingroup$ Ok. I edited my question title to make it a bit more wider. I didn't know concurrency had a link to Curry-Howard. But what about parallelism ? $\endgroup$ – Boris E. Mar 26 '17 at 16:14
  • $\begingroup$ In a functional programming view of Curry-Howard, any (pure) parallelism would occur at the level of proof rewrites and there's usually plenty of it (any time there is multiple redexes). You could add annotations like Haskell's par to control it (i.e. so a less parallel reduction order could be used by default that could be selectively made more parallel) but they would have no logical significance. $\endgroup$ – Derek Elkins Mar 28 '17 at 10:53
4
$\begingroup$

For concurrency in general, there is a very active line of research, which I tried to summarise in this reply: https://cs.stackexchange.com/a/102711/98901

I add here a comment on parallelism, below.


Avron [1996] introduced the notion of hypersequents, i.e., collections of sequents in judgements.

In [Kokke et al., 2019], we showed that a conservative extension of linear logic with hypersequents can be used to type parallelism in process calculi. Essentially, if you have two independent proofs in linear logic of the hypersequent $\mathcal{G}$ and $\mathcal{H}$, respectively, then you can derive $\mathcal{G} | \mathcal{H}$, where $|$ is the operator for composing hypersequents. Following Abramsky's interpretation of "Proofs as Processes" [Abramsky, 1996], we get a typing rule for parallelism: say that you have two independent processes $P$ and $Q$ typed by $\mathcal G$ and $\mathcal H$ respectively; then, the parallel composition $P|Q$ (with $P$ and $Q$ independent) is typed by $\mathcal G | \mathcal H$.

We have just started scratching the surface of the semantic interpretation of this, but that this is parallelism is pretty evident: the semantics of the parallel composition allows for seeing simultaneous actions from both processes, and there is a theorem in the paper stating that neither of the two processes needs to wait for the other to perform at least some action (the Readiness Theorem). The extension to more than two actions at the same time seems straightforward. (The typing already allows for it, but the semantics in that paper does not fully take advantage of it.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.