Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
复制标题
具有答案效果修改的时间验证：具有定界延续的依赖时间类型和效果系统
DOI：
10.1145/3571264
复制
发表时间：
2023
影响因子：
--
通讯作者：
Unno Hiroshi
中科院分区：
文献类型：
--
作者：
Sekiyama Taro;Unno Hiroshi
类型和效果系统是一种广泛使用的程序验证方法，使用类型验证计算结果，使用效果验证其行为。本文扩展了一个效果系统，用于验证时间，值相关的属性产生的事件序列的程序，分隔控制操作符shift 0/reset 0。虽然这些分隔的控制操作符使有用的和强大的编程技术，他们阻碍推理的行为程序，因为他们的能力，暂停，恢复，丢弃，和复制分隔的延续。这个问题在时间属性的有效系统中更为严重，因为这些系统必须能够识别捕获的延续产生的事件序列。我们的关键观察实现有效的推理中存在的分隔控制算子是，它们的使用修改的答案效果，这是时间的延续效果。基于这一观察，我们扩展了时间验证的效果系统，以适应答案效果修改。允许答案效果修改可以轻松地推理捕获的延续产生的痕迹。我们的效果系统的另一个新特性是支持依赖类型的延续，这使我们能够更精确地推理程序。我们证明了有限事件序列的效果系统的可靠性通过类型安全和无限事件序列使用的逻辑关系。
Type-and-effect systems are a widely used approach to program verification, verifying the result of a computation using types, and its behavior using effects. This paper extends an effect system for verifying temporal, value-dependent properties on event sequences yielded by programs, to the delimited control operators shift0/reset0. While these delimited control operators enable useful and powerful programming techniques, they hinder reasoning about the behavior of programs because of their ability to suspend, resume, discard, and duplicate delimited continuations. This problem is more serious in effect systems for temporal properties because these systems must be capable of identifying what event sequences are yielded by captured continuations. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that their use modifies answer effects, which are temporal effects of the continuations. Based on this observation, we extend an effect system for temporal verification to accommodate answer-effect modification. Allowing answer-effect modification enables easily reasoning about traces that captured continuations yield. Another novel feature of our effect system is the support for dependently typed continuations, which allows us to reason about programs more precisely. We prove soundness of the effect system for finite event sequences via type safety and that for infinite event sequences using a logical relation.
登录
查看更多内容
DOI：
--
发表时间：
1986
期刊：
--
影响因子：
--
作者：
William D. Clinger;Daniel P. Friedman;M. Wand
通讯作者：
M. Wand
代表单子
DOI：
10.1145/174675.178047
发表时间：
1994
期刊：
SSRN Electronic Journal
影响因子：
--
作者：
Andrzej Filinski
通讯作者：
Andrzej Filinski
类机器学习语言中异常和控制的概括
DOI：
10.1145/224164.224173
发表时间：
1995
期刊：
Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
影响因子：
--
作者：
Carl A. Gunter;Didier Rémy;J. Riecke
通讯作者：
J. Riecke
抽象控制
DOI：
10.1145/91556.91622
发表时间：
1990
期刊：
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
O. Danvy;Andrzej Filinski
通讯作者：
Andrzej Filinski
具有相关类型的经典序列微积分
DOI：
--
发表时间：
2017
期刊：
European Symposium on Programming
影响因子：
--
作者：
Étienne Miquey
通讯作者：
Étienne Miquey