Thu 27 Aug 2026 15:48 - 16:06 at IP126 Auditorium - Effects, Semantics, and Program Analysis Chair(s): Ben Greenman
We introduce a novel intersection type system for a $\lambda$-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and \emph{expansion}. It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen’s \textsf{HEPCF}.
Thu 27 AugDisplayed time zone: Eastern Time (US & Canada) change
Thu 27 Aug
Displayed time zone: Eastern Time (US & Canada) change
15:30 - 17:00 | Effects, Semantics, and Program AnalysisICFP Papers at IP126 Auditorium Chair(s): Ben Greenman University of Utah | ||
15:30 18mTalk | HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect HandlersRemote ICFP Papers DOI | ||
15:48 18mTalk | When Types Intersect and Effects Get Handled ICFP Papers Stefano Catozi LIPN, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Taro Sekiyama National Institute of Informatics DOI | ||
16:06 18mTalk | Demand-on-Demand Control-Flow Analysis ICFP Papers DOI | ||
16:24 18mTalk | Adequacy for Predicate Transformer Semantics ICFP Papers Kazuki Watanabe National Institute of Informatics; SOKENDAI, Mirai Ikebuchi Kyoto University, Mayuko Kori Research Institute for Mathematical Sciences, Kyoto University DOI | ||
16:42 18mTalk | Misquoted No More: Securely Extracting F* Programs with IO ICFP Papers Cezar-Constantin Andrici MPI-SP, Abigail Pribisova MPI-SP and MPI-SWS, Danel Ahman University of Tartu, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA DOI | ||