弱MSOL性质的类型化
Typing weak MSOL properties
摘要：
我们认为Y-calculus是一种非解释的函数式程序设计语言：程序执行的结果是它的范式，可以看作是对内置操作的调用树。弱一元二阶逻辑（wMSOL）非常适合表达这种树的属性。我们给出了一个类型系统，以确保执行的结果的一个AMDA-Y-程序满足一个给定的wMSOL属性。为了证明该系统的可靠性和完备性，我们构造了一个能够计算wMSOL中表示的属性的Y-calculus的指称语义。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
