Type checking a multithreaded functional language with session types
Type checking a multithreaded functional language with session types
复制标题
DOI：
10.1016/j.tcs.2006.06.028
复制
发表时间：
2006-12
期刊：
影响因子：
--
通讯作者：
V. Vasconcelos;S. Gay;A. Ravara
中科院分区：
文献类型：
--
作者：
V. Vasconcelos;S. Gay;A. Ravara
我们定义了一种语言，其类型系统，将会话类型，允许复杂的协议被指定的类型和静态类型检查验证。与通信信道相关联的会话类型指定协议的状态转换以及与转换相关联的消息的数据类型;因此类型检查可以验证单个消息的正确性和转换序列的正确性。以前，会话类型主要是在π演算的上下文中研究的;相反，我们的公式是基于一个多线程的函数语言与副作用的输入/输出操作。我们的类型判断静态地描述了通道类型的动态变化，我们的函数类型不仅指定了参数和结果类型，而且还描述了通道的变化。我们形式化了我们的语言的语法，语义和类型检查系统，并证明了主题约简和运行时类型安全定理。
We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static type checking. 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 type checking 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 π-calculus; instead, our formulation is based on a multithreaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.