Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.


翻译:舞蹈编程是一种范式,即开发者编写通信系统的全球规格(称为舞蹈),然后自动编译一个按部就班的分布式实施。 不幸的是,有可能写出无法编辑的舞蹈,因为与协议属性有关的问题被称为选择知识。这迫使编程者手工解释可能与他们正在编写的协议相形见绌的执行细节。修正是修复不兼容的舞蹈的自动程序。我们以现有的舞蹈编程正规化为基础,从文献中提出修正的正规化。然而,在将这一程序的预期属性正规化的过程中,我们发现了一个微妙的反比示例,它使原始出版的和同行评审的笔纸理论无效。我们讨论使用标本证明如何使我们找到问题,并表明和证明修正的正确表述。</s>

0
下载
关闭预览

相关内容

专知会员服务
50+阅读 · 2020年12月14日
100+篇《自监督学习(Self-Supervised Learning)》论文最新合集
专知会员服务
164+阅读 · 2020年3月18日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
LibRec 精选:推荐系统的常用数据集
LibRec智能推荐
17+阅读 · 2019年2月15日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
深度学习医学图像分析文献集
机器学习研究会
18+阅读 · 2017年10月13日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
11+阅读 · 2022年9月1日
Arxiv
19+阅读 · 2022年7月29日
Arxiv
10+阅读 · 2021年11月3日
Arxiv
46+阅读 · 2021年10月4日
Arxiv
28+阅读 · 2021年9月18日
Arxiv
14+阅读 · 2020年12月17日
Meta-Learning with Implicit Gradients
Arxiv
13+阅读 · 2019年9月10日
Arxiv
11+阅读 · 2018年9月28日
VIP会员
相关VIP内容
专知会员服务
50+阅读 · 2020年12月14日
100+篇《自监督学习(Self-Supervised Learning)》论文最新合集
专知会员服务
164+阅读 · 2020年3月18日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
LibRec 精选:推荐系统的常用数据集
LibRec智能推荐
17+阅读 · 2019年2月15日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
深度学习医学图像分析文献集
机器学习研究会
18+阅读 · 2017年10月13日
相关论文
Arxiv
11+阅读 · 2022年9月1日
Arxiv
19+阅读 · 2022年7月29日
Arxiv
10+阅读 · 2021年11月3日
Arxiv
46+阅读 · 2021年10月4日
Arxiv
28+阅读 · 2021年9月18日
Arxiv
14+阅读 · 2020年12月17日
Meta-Learning with Implicit Gradients
Arxiv
13+阅读 · 2019年9月10日
Arxiv
11+阅读 · 2018年9月28日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员