CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  External Talks & Seminars  \  External Talk Page Login  
banner bottom
File Top
Logic-Based Domain-Aware Session Types
(Research Talk)

By: Jorge A. Pérez

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.
By example, we argue that our domain-aware session types substantially improve on the expressiveness of existing disciplines. The logical foundations of our framework ensure that well-typed processes enjoy session fidelity, global progress, and termination guarantees

Date: 7 Nov 2013

Location/Event: LIX - Ecole Polytechnique, Paris


File Bottom