Dependent session types via intuitionistic linear type theory

Bernardo Toninho; Luís Caires; Frank Pfenning

doi:10.1145/2003476.2003499

Dependent session types via intuitionistic linear type theory

Bernardo Toninho, Luís Caires, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

70 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 language	English
Title of host publication	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Publisher	ACM - Association for Computing Machinery
Pages	161-171
Number of pages	11
ISBN (Print)	978-145030776-5
DOIs	https://doi.org/10.1145/2003476.2003499
Publication status	Published - 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark Duration: 20 Jul 2011 → 22 Jul 2011

Conference

Conference	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
Country/Territory	Denmark
City	Odense
Period	20/07/11 → 22/07/11

Keywords

π-calculus
Dependent types
Session types
Type theory

Access to Document

10.1145/2003476.2003499

Cite this

@inproceedings{a90489cd330c4ad0aef01f37103f47c2,

title = "Dependent session types via intuitionistic linear type theory",

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.",

keywords = "π-calculus, Dependent types, Session types, Type theory",

author = "Bernardo Toninho and Lu{\'i}s Caires and Frank Pfenning",

year = "2011",

doi = "10.1145/2003476.2003499",

language = "English",

isbn = "978-145030776-5",

pages = "161--171",

booktitle = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

publisher = "ACM - Association for Computing Machinery",

address = "United States",

note = "13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 ; Conference date: 20-07-2011 Through 22-07-2011",

}

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. ACM - Association for Computing Machinery, pp. 161-171, 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011, Odense, Denmark, 20/07/11. https://doi.org/10.1145/2003476.2003499

Dependent session types via intuitionistic linear type theory. / Toninho, Bernardo ; Caires, Luís; Pfenning, Frank.
PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. ACM - Association for Computing Machinery, 2011. p. 161-171.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Dependent session types via intuitionistic linear type theory

AU - Toninho, Bernardo

AU - Caires, Luís

AU - Pfenning, Frank

PY - 2011

Y1 - 2011

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

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

KW - π-calculus

KW - Dependent types

KW - Session types

KW - Type theory

UR - http://www.scopus.com/inward/record.url?scp=80052145663&partnerID=8YFLogxK

U2 - 10.1145/2003476.2003499

DO - 10.1145/2003476.2003499

M3 - Conference contribution

AN - SCOPUS:80052145663

SN - 978-145030776-5

SP - 161

EP - 171

BT - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

PB - ACM - Association for Computing Machinery

T2 - 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011

Y2 - 20 July 2011 through 22 July 2011

ER -

Dependent session types via intuitionistic linear type theory

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this