Hiroshi Unno

Temporal Verification with Answer-Effect Modification

2022 · arXiv (Cornell University)

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 …

On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs

2025 · Proceedings of the ACM on Programming Languages

Applying higher-order model checking techniques to programs that use effect handlers is a major challenge, given the recent undecidability result obtained by Dal Lago and Ghyselen. This challenge has been addressed by using answer-type modifications, …