Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential for program correctness; a session type says what and when should be exchanged through a channel. Central to session-typed languages are sequencing constructs in types and processes that explicitly specify the order of actions in a protocol. In this paper we study session types without sequencing. The resulting framework of minimal session types is arguably the simplest form of session types one could conceive. In the context of a core process calculus with sessions and higher-order concurrency (abstraction-passing), we establish two main technical results. First, we prove that every process $P$ typable with standard session types can be compiled down into a process $\mathcal{D}(P)$ typable with minimal session types. Second, we prove that $P$ and $\mathcal{D}(P)$ are behaviorally equivalent. These results indicate that having sequencing constructs in processes and session types is convenient but redundant: only sequentiality in processes is truly indispensable, as it can correctly codify sequentiality in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow's results in the realm of typed processes, our developments reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into programming languages without sequencing in types.


翻译:届会类型是用于核实信件传递程序的一种基于类型的方法。 届会类型指定了对程序正确性至关重要的通信结构; 届会类型指定了应该通过一个渠道交换的内容和时间。 届会类型的核心语言是以明确指定协议中行动顺序的类型和程序来排序结构。 在本文中, 我们无需顺序来研究届会类型。 由此形成的最小届会类型框架可以说是人们可以想象的最简单的届会类型类型的形式。 在以届会和更高级别货币( 通缩) 进行核心计算的过程中, 我们设定了两个主要的技术结果。 首先, 我们证明每个可使用标准会类型的进程类型的美元( $P$) 都可以被汇编成一个进程 $\ mathcal{D} (P) 的排序。 其次, 我们证明, $P$ 和 $\ mathcall{D} (P) 的排序框架是行为等同的。 这些结果表明, 以进程类型进行进程排序是方便但多余的: 只有进程的顺序是真正不可或缺的, 因为它可以准确地将非顺序编成类型。 我们的发展通过将类型排序方式向方向显示方向的排序, 将方向的顺序显示方向的排序, 方向的顺序显示方向的顺序显示, 方向方向的排序的排序将显示方向的排序进程。

0
下载
关闭预览

相关内容

Processing 是一门开源编程语言和与之配套的集成开发环境(IDE)的名称。Processing 在电子艺术和视觉设计社区被用来教授编程基础,并运用于大量的新媒体和互动艺术作品中。
【硬核书】树与网络上的概率,716页pdf
专知会员服务
72+阅读 · 2021年12月8日
【新书】贝叶斯网络进展与新应用,附全书下载
专知会员服务
119+阅读 · 2019年12月9日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
征稿 | CFP:Special Issue of NLP and KG(JCR Q2,IF2.67)
开放知识图谱
1+阅读 · 2022年4月4日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年3月8日
Arxiv
0+阅读 · 2023年3月6日
Arxiv
12+阅读 · 2022年11月21日
Arxiv
64+阅读 · 2021年6月18日
Arxiv
49+阅读 · 2021年5月9日
VIP会员
相关VIP内容
【硬核书】树与网络上的概率,716页pdf
专知会员服务
72+阅读 · 2021年12月8日
【新书】贝叶斯网络进展与新应用,附全书下载
专知会员服务
119+阅读 · 2019年12月9日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
征稿 | CFP:Special Issue of NLP and KG(JCR Q2,IF2.67)
开放知识图谱
1+阅读 · 2022年4月4日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
相关论文
Arxiv
0+阅读 · 2023年3月8日
Arxiv
0+阅读 · 2023年3月6日
Arxiv
12+阅读 · 2022年11月21日
Arxiv
64+阅读 · 2021年6月18日
Arxiv
49+阅读 · 2021年5月9日
相关基金
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员