Typing weak MSOL properties

Sylvain Salvati; Igor Walukiewicz

doi:10.23638/LMCS-13(1:14)2017

Sylvain Salvati ; Igor Walukiewicz - Typing weak MSOL properties

lmcs:3215 - Logical Methods in Computer Science, March 23, 2017, Volume 13, Issue 1 - https://doi.org/10.23638/LMCS-13(1:14)2017

Typing weak MSOL propertiesArticle

Authors: Sylvain Salvati ; Igor Walukiewicz

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.

https://doi.org/10.23638/LMCS-13(1:14)2017

Source: arXiv.org:1609.02753

Volume: Volume 13, Issue 1

Published on: March 23, 2017

Accepted on: March 23, 2017

Submitted on: March 23, 2017

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute