Value-Dependent Session Design in a Dependently Typed Language
Value-Dependent Session Design in a Dependently Typed Language
复制标题
DOI：
10.4204/eptcs.291.5
复制
发表时间：
2019-04
期刊：
影响因子：
--
通讯作者：
Jan de Muijnck-Hughes;Edwin C. Brady;W. Vanderbauwhede
中科院分区：
文献类型：
--
作者：
Jan de Muijnck-Hughes;Edwin C. Brady;W. Vanderbauwhede
会话类型提供了一种类型规则，允许在类型检查期间使用协议规范，从而确保实现遵循给定的规范。在使用依赖类型语言实现全局会话类型时，必须注意在描述中引入的值被知道该值的角色使用。我们提出了Sessions，一个资源依赖的EDSL，用于在依赖类型语言Idris中描述全局会话描述。当我们构造会话描述时，参数化edsl类型的值跟踪它们遇到的角色和消息。我们可以使用这些知识来确保消息值只被知道该值的人使用。会话支持可计算的、可组合的、高阶的、依赖于值的协议描述。我们通过描述TCP握手、提供回显和基本算术操作的多模态服务器以及支持身份验证交互步骤的高阶协议来演示会话的表达性。
Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value. We present Sessions, a Resource Dependent EDSL for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs' type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step.