SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Sat 18 Oct 2025 11:00 - 11:15 at Orchid East - Type 2

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, the use of a monomorphic version of which allows to recover decidability. However, the absence of polymorphism leads to a loss of modularity, reusability, and even expressivity. In this work, we study the problem of defining a calculus that on the one hand supports answer-type polymorphism and subtyping but on the other hand ensures the underlying model checking problem to remain decidable. The solution proposed in this paper is based on the introduction of the polymorphic answer-type $\Box$ whose role is to provide a good compromise between expressiveness and decidability, the latter demonstrated through the construction of a selective type-directed CPS transformation targeting a calculus \emph{without} effect handlers and any form of polymorphism. Noticeably, the introduced calculus allows the answer types of effects implemented by tail-resumptive effect handlers to be polymorphic. We also implemented a proof-of-concept model checker for the new calculus.

This program is tentative and subject to change.

Sat 18 Oct

Displayed time zone: Perth change

10:30 - 12:15
10:30
15m
Talk
Borrowing From Session Types
OOPSLA
Hannes Saffrich University of Freiburg, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon
10:45
15m
Talk
Modal Effect Types
OOPSLA
Wenhao Tang The University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Daniel Hillerström Category Labs and The University of Edinburgh, Sam Lindley The University of Edinburgh, Anton Lorenzen University of Edinburgh
11:00
15m
Talk
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
OOPSLA
Taro Sekiyama National Institute of Informatics, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Hiroshi Unno Tohoku University
11:15
15m
Talk
Proof Repair across Quotient Type Equivalences
OOPSLA
Cosmo Viola University of Illinois Urbana-Champaign, Max Fan Cornell University, Talia Lily Ringer University of Illinois Urbana-Champaign
11:30
15m
Talk
Structural Information Flow: A Fresh Look at Types for Non-Interference
OOPSLA
Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University
Pre-print
11:45
15m
Talk
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
OOPSLA
Jiří Beneš University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
Pre-print
12:00
15m
Talk
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
OOPSLA
Patrick LaFontaine Purdue University, Zhe Zhou Purdue University, Ashish Mishra IIT Hyderabad, Suresh Jagannathan Purdue University, Benjamin Delaware Purdue University