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.