Wed 18 Jan 2023 11:10 - 11:35 at Avenue34 - Types I Chair(s): Neel Krishnaswami

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.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:45 - 12:00
Types IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:45
25m
Talk
Higher-Order Leak and Deadlock Free LocksDistinguished Paper
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University
DOI
11:10
25m
Talk
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
POPL
Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI
11:35
25m
Talk
Recursive Subtyping for All
POPL
Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI