一句话：为带代数效应与处理器的 λ-演算提出首个兼具终止刻画与可达性归约能力的交集类型系统。
本文为带代数效应与处理器的 λ-演算引入一种新的交集类型系统。该系统本质上是行为性的，满足交集类型系统的经典性质，包括主语归约与主语展开。由此，它既能刻画项的求值过程终止，又能将可达性问题归约到类型推断。这是首个为带处理器演算同时具备这些特征的系统。此外，它还诱导出一个简单类型系统：该系统虽不保证终止，但类型可靠，且其 HOMC 问题是可判定的，这与 Dal Lago 和 Ghyselen 的 HEPCF 等相关系统不同。
We introduce a novel intersection type system for a λ-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 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 HEPCF.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CatoziLS26,
title = {When Types Intersect and Effects Get Handled},
author = {Stefano Catozi and Ugo Dal Lago and Taro Sekiyama},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828707}
}