paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics

基于可实现性语义的简单类型 λμ-演算的修正完备性结果
LMCS vol.Volume 13, Issue 32017匹配度 1/10 · 该论文属于纯类型论/形式语义领域，研究简单类型 λμ-演算的可实现性语义与完备性，与用户关注的 ML/Agentic 程序静态分析、LLM 与程序分析/形式化验证交叉、浮点程序分析或贝叶斯程序分析均无直接关联。引用 2 inbox
Karim Nour, Mohamad Ziadeh
类型系统形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：为简单类型 λμ-演算提出新的可实现性语义，并用项模型证明其完备性，修正了此前工作中的错误。

本文针对简单类型 λμ-演算，重新审视其可实现性语义与完备性证明。作者定义了一种新的可实现性语义，并证明可靠性：若项可类型化，则它居留其类型解释。随后，他们通过构造一个特定的项模型证明该语义的完备性，即语义中可居留的类型均可由合适项类型化。该工作修正了第一作者与 Saber 此前论文中的若干错误，为带经典控制算子的简单类型演算提供了更可靠的语义基础。

问题
为简单类型 λμ-演算建立可靠的可实现性语义，并修正已有完备性证明中的错误。
方法
定义新的可实现性语义，证明可类型化项居留其类型解释，并利用特定项模型证明完备性。
评估
通过理论证明评估，包括可靠性定理与基于项模型的完备性定理，不涉及实现或实验。
原文摘要（Abstract）

In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. We also prove a completeness result of our realizability semantics using a particular term model. This paper corrects some errors in [21] by the first author and Saber.Comment: arXiv admin note: text overlap with arXiv:0905.0357

链接与引用

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

BibTeX 
@article{NourZ16,
  title = {A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics},
  author = {Karim Nour and Mohamad Ziadeh},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 3},
  year = {2017},
  doi = {10.23638/lmcs-13(3:13)2017}
}