Logical Foundations of Session Types

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).