Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Salvati, Sylvain; Walukiewicz, Igor http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-54173
URL:

;

A Model for Behavioural Properties of Higher-order Programs

pdf-format:


Abstract

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.

BibTeX - Entry

@InProceedings{salvati_et_al:LIPIcs:2015:5417,
  author =	{Sylvain Salvati and Igor Walukiewicz},
  title =	{{A Model for Behavioural Properties of Higher-order Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{229--243},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5417},
  URN =		{urn:nbn:de:0030-drops-54173},
  doi =		{10.4230/LIPIcs.CSL.2015.229},
  annote =	{Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models}
}

Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models
Seminar: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue date: 2015
Date of publication: 2015


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI