paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Typing weak MSOL properties

弱 MSOL 性质的类型化
LMCS vol.Volume 13, Issue 12017匹配度 2/10 · 该论文是纯类型系统与形式语义工作，用类型系统保证 λY 程序正规形满足 wMSOL 性质，属于传统形式化验证/静态分析范畴，但与用户核心关注的 AI×PL 交叉方向（LLM/Agent 用于静态分析或形式化验证、浮点/贝叶斯程序分析与 LLM 结合）没有直接关联。引用 11 inbox
Sylvain Salvati, Igor Walukiewicz
类型系统形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：为 λY 演算设计类型系统，确保程序正规形满足给定的弱一元二阶逻辑性质。

本文研究如何静态保证非解释函数式程序 λY 的执行结果满足给定的弱一元二阶逻辑（wMSOL）性质。程序执行结果为其正规形，可看作对内置操作的调用树，而 wMSOL 适合描述此类树的性质。作者为 λY 演算设计了一个类型系统，使得良类型程序的结果满足指定 wMSOL 性质。为证明该系统的可靠性与完备性，他们构造了 λY 的指称语义，使其能够计算 wMSOL 表达的性质。评估以理论证明为主，未涉及实现或实验。

问题
如何保证 λY 程序执行得到的正规形（内置操作调用树）满足给定的 wMSOL 性质。
方法
为 λY 演算设计类型系统，并构造能计算 wMSOL 性质的指称语义，用以证明类型系统的可靠性（soundness）与完备性（completeness）。
评估
通过构造指称语义并证明 soundness/completeness 进行理论评估；摘要未提及实现或实验。
原文摘要（Abstract）

We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We give a type system for ensuring that the result of the execution of a lambda-Y-program satisfies a given wMSOL property. In order to prove soundness and completeness of the system we construct a denotational semantics of lambda-Y-calculus that is capable of computing properties expressed in wMSOL.

链接与引用

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

BibTeX 
@article{SalvatiW15,
  title = {Typing weak MSOL properties},
  author = {Sylvain Salvati and Igor Walukiewicz},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 1},
  year = {2017},
  doi = {10.23638/lmcs-13(1:14)2017}
}