CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
Logic-Based Domain-Aware Session Types
{ Wed, 4 Dec 2013, 14h00 }

By: Jorge A. Pérez

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.


Hosted by: Software Systems

Location: DI seminars room

File Bottom