文章基本信息

标题：A Model for Behavioural Properties of Higher-order Programs
本地全文：下载
作者：Sylvain Salvati ; Igor Walukiewicz
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：229-243
DOI：10.4230/LIPIcs.CSL.2015.229
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.
关键词：Simply typed lambda-Y-calculus; Monadic second order logic; semantic models