patternMinor
What is the current status of parallel or concurrent programs in the Curry-Howard isomorphism?
Viewed 0 times
thewhathowardstatuscurryparallelcurrentprogramsconcurrentisomorphism
Problem
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 ?
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 ?
Solution
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.)
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.)
Context
StackExchange Computer Science Q#72048, answer score: 7
Revisions (0)
No revisions yet.