Session Types for Functional Multithreading

机译：功能性多线程的会话类型

获取原文

获取原文并翻译 | 示例

页面导航

摘要
著录项
相似文献
相关主题

摘要

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 π-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 rules of our language, and prove subject reduction and runtime type safety theorems.

机译：我们定义了一种语言，该语言的类型系统结合了会话类型，允许按类型指定复杂协议并通过静态类型检查进行验证。与通信信道相关的会话类型指定协议的状态转换以及与转换相关的消息的数据类型；因此，类型检查可以验证单个消息的正确性和转换序列的正确性。以前，会话类型主要是在π演算的背景下研究的。相反，我们的表述基于具有副作用的输入/输出操作的多线程功能语言。我们的打字判断静态地描述了通道类型的动态变化，我们的通道类型静态地跟踪了别名，我们的函数类型不仅指定了参数和结果类型，而且还描述了通道的变化。我们对语言的语法，语义和键入规则进行形式化，并证明主题缩减和运行时类型安全定理。

著录项

来源
《International Conference on Concurrency Theory(CONCUR 2004); 20040831-20040903; London; GB》|2004年|P.497-511|共15页
会议地点 London(GB);London(GB)
作者
Vasco Vasconcelos; Antonio Ravara; Simon Gay;
展开▼
作者单位

Departamento de Informatica, Faculdade de Ciencias, Universidade de Lisboa, 1749-016 Lisboa, Portugal;

展开▼
会议组织
原文格式 PDF
正文语种 eng
中图分类 TP393.01;
关键词
session types; static typechecking; concurrent programming; specification of communication protocols;

机译：会话类型；静态类型检查；并发编程；通信协议的规范;

相似文献

外文文献
中文文献
专利

1. Type checking a multithreaded functional language with session types [J] . Vasco T. Vasconcelos, Simon J. Gay, Antonio Ravara Theoretical computer science . 2006,第1a2期

机译：使用会话类型进行类型检查多线程功能语言
2. Classroom-Based Micro-Sessions of Functional High-Intensity Circuit Training Enhances Functional Strength but Not Cardiorespiratory Fitness in School Children—A Feasibility Study [J] . Florian A. Engel, Matthias Oliver Wagner, Franziska Schelhorn, Frontiers in Public Health . 2019,第a期

机译：基于教室的功能高强度电路训练的微观会增强功能强度，但在学校儿童中没有心肺刺激性健身 - 可行性研究
3. Classroom-Based Micro-Sessions of Functional High-Intensity Circuit Training Enhances Functional Strength but Not Cardiorespiratory Fitness in School Children—A Feasibility Study [J] . Engel Florian A., Wagner Matthias Oliver, Schelhorn Franziska, Frontiers in Public Health . 2019,第2期

机译：基于教室的功能高强度电路训练的微观会增强功能强度，但在学校儿童中没有心肺气体健身 - 一个可行性研究
4. Session types for linear multithreaded functional programming [C] . Vasco T. Vasconcelos Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming . 2009

机译：线性多线程功能编程的会话类型
5. Personalizing information retrieval using interaction behaviors in search sessions in different types of tasks. [D] . Liu, Chang. 2012

机译：使用不同类型任务中搜索会话中的交互行为来个性化信息检索。
6. Classroom-Based Micro-Sessions of Functional High-Intensity Circuit Training Enhances Functional Strength but Not Cardiorespiratory Fitness in School Children—A Feasibility Study [O] . Florian A. Engel, Matthias Oliver Wagner, Franziska Schelhorn, 2019

机译：基于教室的功能性高强度电路训练的微型课程可增强小学生的功能强度但不能增强心肺功能的适应性研究
7. Type checking a multithreaded functional language with session types [O] . Vasconcelos Vasco T., Gay Simon J., Ravara António 2006

机译：使用会话类型进行类型检查多线程功能语言

Session Types for Functional Multithreading

摘要

著录项

相似文献

相关主题

期刊订阅