Dependent session types via intuitionistic linear type theory

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Citations (Scopus)

Abstract

We develop an interpretation of linear type theory as dependent session types for a term passing extension of the π-calculus. The type system allows us to express rich constraints on sessions, such as interface contracts and proof-carrying certification, which go beyond existing session type systems, and are here justified 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.

Original languageEnglish
Title of host publicationPPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
PublisherAssociation for Computing Machinery (ACM)
Pages161-171
Number of pages11
ISBN (Print)978-145030776-5
DOIs
Publication statusPublished - 2011
Event13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark
Duration: 20 Jul 201122 Jul 2011

Conference

Conference13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
CountryDenmark
CityOdense
Period20/07/1122/07/11

Keywords

  • π-calculus
  • Dependent types
  • Session types
  • Type theory

Fingerprint Dive into the research topics of 'Dependent session types via intuitionistic linear type theory'. Together they form a unique fingerprint.

  • Cite this

    Toninho, B., Caires, L., & Pfenning, F. (2011). Dependent session types via intuitionistic linear type theory. In PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming (pp. 161-171). Association for Computing Machinery (ACM). https://doi.org/10.1145/2003476.2003499