2026-07-26T05:32:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5417 2024-03-06T10:36:25Z ddc:004 open_access

A Model for Behavioural Properties of Higher-order Programs Salvati, Sylvain Walukiewicz, Igor Simply typed lambda-Y-calculus Monadic second order logic semantic models 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sylvain Salvati and Igor Walukiewicz 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.229 urn:nbn:de:0030-drops-54173 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.229 eng https://creativecommons.org/licenses/by/3.0/legalcode