文章基本信息

标题：Typing weak MSOL properties
本地全文：下载
作者：Walukiewicz, Igor ; Salvati, Sylvain
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2017
卷号：13
期号：1
语种：English
出版社：Technical University of Braunschweig
摘要：We consider lambda-Y-calculus as a non-interpreted functional programminglanguage: the result of the execution of a program is its normal form that canbe seen as the tree of calls to built-in operations. Weak monadic second-orderlogic (wMSOL) is well suited to express properties of such trees. We give atype system for ensuring that the result of the execution of a lambda-Y-programsatisfies a given wMSOL property. In order to prove soundness and completenessof the system we construct a denotational semantics of lambda-Y-calculus thatis capable of computing properties expressed in wMSOL.
关键词：Computer Science - Logic in Computer Science