Nov 21, 2017: Jorge A. Pérez: Logical Foundations for Message-Passing Concurrency

November 21, 2017Logical Foundations for Message-Passing Concurrency
Room: Hal B 2AJorge A. Pérez

The so-called Curry-Howard(-de Bruijn) isomorphism is key to the
theory of programming languages: it tightly relates, on the one hand,
logical propositions and types; on the other hand, it connects proofs
and functional programs. This isomorphism has proved essential to
endow reasoning techniques over sequential programs with clean
principles, which have both operational and logical meanings.

In 2010, Caires and Pfenning put forward an interpretation of linear
logic propositions as session types for communicating processes.
Remarkably, this result defines a
propositions-as-types/proofs-as-programs correspondence, in the style
of the Curry-Howard isomorphism, but in the context of
message-passing, concurrent processes in the pi-calculus.

In this talk, I will give an overview to Caires and Pfenning's
interpretation, from the perspective of languages for concurrency. I
will also overview two recent further developments:
- The first concerns the analysis of choreographies (multiparty
protocols) using the (binary) type discipline induced by Caires and
Pfenning's interpretation.
- The second result extends Caires and Pfenning's interpretation with
(internal) non-determinism and abortable behaviors.

If time permits, I will also discuss ongoing work aimed at
systematising different type systems for concurrency under the
canonical perspective of Caires and Pfenning's interpretation.