Browse our site
About
People
Research Areas
Projects
Publications
Seminars
Future
Past
News
You are here:
Home
Seminars
Past
Logic-Based Domain-Aware Session Types
CENTRIA seminar: Logic-Based Domain-Aware Session Types
Main information
By:
Jorge A. Perez (Universidade Nova de Lisboa)
Date:
Wednesday, 4th of December 2013, 14h00
Location:
FCT/UNL, Seminar Room (Ed. II)
Abstract
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.
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.
Short-bio
Jorge A. Pérez (http://www.jorgeaperez.net/) is a postdoc at CITI, Universidade NOVA de Lisboa (Portugal). Broadly interested in concurrency theory, he currently works on type-based analysis for models of concurrent communication. In May 2010, he obtained a PhD in Informatics from the University of Bologna, Italy (supervisor: Davide Sangiorgi). His thesis studies principles and reasoning techniques for formal models of concurrent, distributed processes with code mobility. Before that, in February 2006, he earned an Engineering Degree in Computer Science at the Universidad Javeriana (Colombia). His research thesis, supervised by Camilo Rueda, was on the intersection of concurrency and constraint programming.
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541
