一句话：提出支持 shift0/reset0 的依赖时序类型与效应系统，通过 answer-effect 修改实现事件序列的时序验证。
类型与效应系统常用类型描述计算结果、效应描述程序行为。本文将验证程序所产生事件序列上时序且值依赖性质的效果系统扩展到 shift0/reset0 定界控制操作符。这些操作符可暂停、恢复、丢弃和复制定界续延，使行为推理困难；时序效应系统还需识别被捕获续延产生的事件序列。关键观察是其使用会修改 answer effect，即续延的时序效应。本文据此扩展效果系统以允许 answer-effect 修改，并支持依赖类型续延，从而更精确推理程序。健全性上，有限事件序列由类型安全证明，无限事件序列由逻辑关系证明。
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.
@article{paperbot2076,
title = {Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations},
author = {Taro Sekiyama and Hiroshi Unno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571264}
}