Temporal Verification with Answer-Effect Modification

TL;DR

This paper extends effect systems for verifying temporal, value-dependent properties in programs to include delimited control operators, enabling precise reasoning about complex control flow and event sequences.

Contribution

It introduces an effect system that accounts for answer-effect modification and supports dependently-typed continuations for improved temporal verification.

Findings

Proves soundness of the extended effect system for finite event sequences.

Demonstrates reasoning capabilities with answer-effect modification.

Supports dependently-typed continuations for more precise analysis.

Abstract

Type-and-effect systems are a widely-used approach to program verification, verifying the result of a computation using types, and the 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.