paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus

源自无类型 λ 演算稳定模型的一个经典可实现性模型
LMCS vol.Volume 13, Issue 42017匹配度 2/10 · 论文属于纯形式语义/经典可实现性理论，讨论无类型λ演算的稳定模型与可数选择，与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。仅因同属程序语言理论范畴而有非常宽泛的联系。引用 5 inbox
Thomas Streicher
形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：从相干空间的无类型 λ 演算稳定模型构造经典可实现性模型，并用 bar recursion/induction 验证可数选择。

本文研究 J.-L. Krivine 意义下的经典可实现性模型。作者从相干空间（coherence spaces）中一个无类型 λ 演算的稳定模型出发，构造相应的经典可实现性模型，并分析其可验证的逻辑原则。关键结果是：该模型借助 bar recursion 与 bar induction 可验证可数选择（countable choice）。这一工作将无类型 λ 演算的稳定模型、相干空间语义与经典可实现性联系起来，为理解选择原则在可实现性模型中的有效性提供了新的语义视角。

问题
如何从相干空间中的无类型 λ 演算稳定模型构造 Krivine 经典可实现性模型，并确定其能验证哪些逻辑原则，尤其是可数选择。
方法
作者以相干空间中的无类型 λ 演算稳定模型为起点构造经典可实现性模型，并通过 bar recursion 与 bar induction 证明可数选择在该模型中有效。
评估
评估为理论语义分析：给出模型并证明其验证可数选择，未涉及实现或实验基准。
原文摘要（Abstract）

We study a classical realizability model (in the sense of J.-L. Krivine) arising from a model of untyped lambda calculus in coherence spaces. We show that this model validates countable choice using bar recursion and bar induction.

链接与引用

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

BibTeX 
@article{Streicher17,
  title = {A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus},
  author = {Thomas Streicher},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 4},
  year = {2017},
  doi = {10.23638/lmcs-13(4:24)2017}
}