Dependent Session Types via Intuitionistic Linear Type Theory
Jul 2011
We develop an interpretation of linear type theory as dependent session types for a term passing extension of the pi-calculus. The type system allows us to express rich constraints on sessions, such as interface contracts and proof carrying certi cation, which go beyond existing session type systems, and are here justi fied on purely logical grounds.
We can further refine our interpretation using proof irrelevance to eliminate communication overhead for proofs between trusted parties. Our technical results include type preservation and global progress, which in our setting naturally imply compliance to all properties declared in interface contracts expressed by dependent types.
