You are here

Logical Foundations of Session Types

20 March 2012
Ex Boccherini - Piazza S. Ponziano 6 (Conference Room )
We overview a type theoretic foundation for distributed processes, based on a Curry-Howard logical interpretation of session types as logical propositions of (classical, in this talk) linear logic. Natural extensions of the basic framework include dependent types, allowing us to describe rich interface contracts and proof carrying code, and modal types, allowing us to express digital certificates and proof irrelevance (joint work with Frank Pfenning and Bernardo Toninho).
Caires, Luis