Session types for functional multithreading
Abstract
We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously session types have mainly been studied in the context of the pi-calculus; instead, our formulation is based on a multi-threaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and typing system of our language, and prove subject reduction and runtime type safety theorems. We also present a type checking algorithm and show that it is correct with respect to the type system.
@InProceedings\{vasconcelos.etal:session-types-functional-multithreading,
author = \{V. Vasconcelos and A. Ravara and S. Gay},
title = \{Session types for functional multithreading},
booktitle = \{CONCUR '04},
year = \{2004},
pages = \{497--511},
volume = \{3170},
series = \{LNCS},
publisher = \{SPRINGER},
url = \{http://mikado.di.fc.ul.pt/repository/vasconcelos.etal_session-types-functional-multithreading.pdf}
}
About this site. Last modified: Thu Apr 25 11:11:27 CEST 2024