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 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
18m
Talk
HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect HandlersRemote
ICFP Papers
Tim Whiting Brigham Young University, Kimball Germane Brigham Young University
DOI
15:48
18m
Talk
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
18m
Talk
Demand-on-Demand Control-Flow Analysis
ICFP Papers
Chahyun Kang Brigham Young University, Kimball Germane Brigham Young University
DOI
16:24
18m
Talk
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
18m
Talk
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