paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Complete Call-by-Value Calculi of Control Operators II: Strong Termination

控制算子的完备传值调用演算 II：强终止性
LMCS vol.Volume 17, Issue 12021匹配度 2/10 · 该论文属于纯粹的编程语言理论工作，研究 lambda-mu 演算、控制操作符、强终止性与 CPS 语义/类型系统，并未涉及静态分析、机器学习系统、Agentic 程序或 LLM，因此与用户的核心研究方向基本不匹配。引用 0 inbox
Ryu Hasegawa
类型系统形式语义
crossref: 2026-09-10

AI 速览

一句话：本文刻画了 CCV lambda-mu 演算的强终止性，并给出其与 CPS 语义及类型可推导性的等价表征。

本文是控制算子完备传值调用演算系列的第二篇，研究第一部分提出的 CCV lambda-mu 演算。该演算相对标准 CPS（continuation-passing style）语义是完备的，前作已为其建立并交类型系统。本文关注项的强终止性（strong termination / 强规范化），目标是在语义与类型两个层面给出精确刻画。作者证明，项的强可规范化可由其在 CPS 语义下的行为以及在该并交类型系统中的可类型化性来表征，从而将强终止性、CPS 语义与类型可推导性联系起来。本文以理论证明与表征定理为主要评估，说明该类型系统能够捕获控制算子演算的强终止性质。

问题
如何刻画 CCV lambda-mu 演算中项的强终止性（强可规范化性）？
方法
基于该演算的 CPS 语义与已有的并交类型系统，给出强终止性与 CPS 语义行为及类型可类型化性之间的表征定理。
评估
以理论证明与表征定理为主，说明该类型系统能够刻画该控制算子演算的强终止性。
原文摘要（Abstract）

We provide characterization of the strong termination property of the CCV (complete call-by-value) lambda-mu calculus introduced in the first part of this series of the paper. The calculus is complete with respect to the standard continuation-passing style (CPS) semantics. The union-intersection type systems for the calculus is developed in the previous paper. We characterize the strong normalizability of terms of the calculus in terms of the CPS semantics and typeability.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot1333,
  title = {Complete Call-by-Value Calculi of Control Operators II: Strong Termination},
  author = {Ryu Hasegawa},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 1},
  year = {2021},
  doi = {10.23638/lmcs-17(1:18)2021}
}