Delimited control operators—such as shift/reset and algebraic effect handlers—offer a unified and structured way to express a wide range of effectful programs. However, the control operators complicate program verification problems due to their ability to suspend, resume, duplicate, and discard continuations. Answer-type modification (ATM), a type-theoretic concept introduced by Danvy and Filinski in 1990, provides a powerful means to statically track the dynamic changes in continuations caused by the delimited control operators.

In this talk, I will present our recent work on incorporating ATM into various type-based verification frameworks. Specifically, I will describe how ATM can be integrated with a refinement type system, sequential effect system, and higher-order model checking to enable precise and practical verification of higher-order effectful programs that utilize algebraic effect handlers. Through these developments, we demonstrate how ATM serves as a foundation for reasoning about advanced control effects in modern programming languages.

I’m an associate professor at National Institute of Informatics in Japan. I am interested in theory and applications of programming languages, such as type theory, program verification, type inference, program reasoning, and so on.