Dependent Temporal Type-and-Effect System with Delimited Continuations
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 how computations yielding event sequences are manipulated by the control operators. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that the use of them modifies not only answer types but also the temporal effects of contexts. This observation enables the integration of an effect system for temporal verification with a type system that accommodates answer-type modification. 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.
Sun 11 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
16:00 - 17:30
|Dependent Temporal Type-and-Effect System with Delimited Continuations
|Enabling Safe Shared-Memory Interoperability in WebAssemblyVirtual
|Verifying non-terminating programs with IO in F*
Cezar-Constantin Andrici MPI-SP, Theo Winterhalter MPI-SP, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of TechnologyPre-print File Attached