What is the current status of parallel or concurrent programs in the Curry-Howard isomorphism?

Question

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 ?

Answer 1

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.)

Answer 2

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.)