APLAS 2025
Mon 27 - Thu 30 October 2025 Bengaluru, India

This program is tentative and subject to change.

Tue 28 Oct 2025 14:00 - 14:30 at R104 - Control, Effects, and Decidability Chair(s): Sanjiva Prasad

It is well known that the reachability for simply-typed lambda calculus with recursive definitions and finite base-type values (finitary PCF) is decidable. A recent paper by Dal Lago and Ghyselen has shown that the same problem becomes undecidable when the language is extended with algebraic effect and handlers (effect handlers). We show that, perhaps surprisingly, the problem becomes decidable even with effect handlers when the type system is extended with answer type modification (ATM). A natural intuition may find the result contradictory, because one would expect allowing ATM makes more programs typable. Indeed, this intuition is correct in that there are programs that are typable with ATM but not without it, as we shall show in the paper. However, a corollary of our decidability result is that the converse is true as well: there are programs that are typable without ATM but becomes untypable with ATM, and we will show concrete examples of such programs in the paper. Our decidability result is proven by a novel continuation passing style (CPS) transformation that transforms an ATM-typable finitary PCF program with effect handlers to a finitary PCF program without effect handlers. Additionally, as another application of our CPS transformation, we show that every recursive-function-free ATM-typable finitary PCF program with effect handlers terminates, while there are (necessarily ATM-untypable) recursive-function-free finitary PCF programs with effect handlers that may diverge. Finally, we disprove a claim made in a recent work that proved a similar but strictly weaker decidability result. We foresee our decidability result to lay a foundation for developing verification methods for programs with effect handlers, just as the decidability result for reachability of finitary PCF has done such for programs without effect handlers.

This program is tentative and subject to change.

Tue 28 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

14:00 - 15:30
Control, Effects, and DecidabilityResearch Papers at R104
Chair(s): Sanjiva Prasad Indian Institute of Technology Delhi
14:00
30m
Talk
Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
Research Papers
Ryunosuke Endo Waseda University, Tachio Terauchi Waseda University
14:30
30m
Talk
Expressive Power of One-Shot Control Operators and CoroutinesIn Person Talk
Research Papers
Kentaro Kobayashi University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba
15:00
30m
Talk
Positive Sharing and Abstract MachinesRemote Talk
Research Papers
Beniamino Accattoli Inria & Ecole Polytechnique, Claudio Sacerdoti Coen University of Bologna, Jui-Hsuan Wu CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668