Detail

Logic-Based Domain-Aware Session Types

Session types are type-based abstractions of interactive behavior in
communication-centric systems.
They allow to verify the correctness of distributed software artifacts
via static type-checking.
In prior work, an interpretation of linear logic propositions as
session types for communicating processes was proposed.
In a concurrent setting, it defines a tight
propositions-as-types/proofs-as-programs correspondence, in the style
of the Curry-Howard isomorphism.

In this talk, I will present a generalization of such an
interpretation, which relies on a variant of intuitionistic linear
logic with hybrid logic constructs, obtaining a system reminiscent of
modal logic.
The resulting type structure enhances usual abstractions of protocols
as sessions with explicit descriptions of the domains in which
protocol participants interact and may migrate to.
As domains are governed by a parametric accessibility relation,
flexible access and connectedness relationships among domains can be
elegantly defined and statically enforced.
Our framework can account for non trivial scenarios in which domain
information is only known at runtime.

Joint work with Luís Caires, Frank
Pfenning, and Bernardo Toninho.