Dependent Session Types via Intuitionistic Linear Type Theory

Frank Pfenning, Carnegie Mellon University, USA

(Joint work with Luis Caires and Bernardo Toninho)

In prior work, we have developed an interpretation of an intuitionistic linear propositions as session types, where concurrent programs can be extracted from sequent proofs. We report on current research to extend this to a linear type theory in order to obtain dependent session types that can express complex constraints on sessions, including interface contracts and proof-carrying certification. One important idea seems to be proof irrelevance, which can be employed to reduce communication overhead between trusted parties.