Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 14-minute conference presentation from OOPSLA 2025 that addresses the significant challenge of applying higher-order model checking techniques to programs using effect handlers. Learn how researchers Taro Sekiyama, Ugo Dal Lago, and Hiroshi Unno tackle the undecidability issues identified in recent work by Dal Lago and Ghyselen through innovative answer-type modifications. Discover their proposed solution featuring a new calculus that supports answer-type polymorphism and subtyping while maintaining decidability in the underlying model checking problem. Examine the introduction of the polymorphic answer-type â–¡ as a compromise between expressiveness and decidability, demonstrated through a selective type-directed CPS transformation targeting a calculus without effect handlers or polymorphism. Understand how the HEPCFâ–¡ATM calculus enables polymorphic answer types for effects implemented by tail-resumptive effect handlers, and explore the practical implementation of their proof-of-concept model checker. Gain insights into cutting-edge research in programming language theory, algebraic effect handlers, and formal verification methods presented at one of the premier conferences in object-oriented programming systems, languages, and applications.
