Typing weak MSOL properties
Logic in Computer Science
2019-03-14 v2
Abstract
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.
Cite
@article{arxiv.1609.02753,
title = {Typing weak MSOL properties},
author = {Sylvain Salvati and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1609.02753},
year = {2019}
}