一句话：提出支持高阶效应操作处理器的核心演算，处理器由无律原始 Monad 承载而计算判断满足判断性 Monad 律，并给出语义模型与元定理。
论文研究带高阶效应操作处理器的编程语言设计；这类操作可把计算作为参数或返回计算。作者提出并分析一个核心演算，支持高阶 kind 的 impredicative 多态、高阶效应操作处理器以及可选的通用递归。其独特设计是：处理器由无律的原始 Monad 承载，而计算判断仍在判断层面满足 Monad 律。作者在逻辑框架中形式化该演算，并用可实现性语义给出指称模型；针对无递归片段，利用 synthetic Tait computability 与一种新的 ⊤⊤-lifting 技术证明闭项典范性和参数性。
This paper studies the design of programming languages with handlers of higher-order effectful operations - effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative polymorphism, handlers of higher-order effectful operations, and optionally general recursion. The distinctive design choice of this calculus is that handlers are carried by lawless raw monads, while the computation judgements still satisfy the monadic laws judgementally. We present the calculus with a logical framework and give denotational models of the calculus using realizability semantics. We prove closed-term canonicity and parametricity for the recursion-free fragment of the language using synthetic Tait computability and a novel form of the ⊤⊤-lifting technique.
@article{paperbot3903,
title = {Handling Higher-Order Effectful Operations with Judgemental Monadic Laws},
author = {Zhixuan Yang and Nicolas Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776678}
}