episciences.org_3215_1638768408
1638768408
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
1860-5974
03
23
2017
Volume 13, Issue 1
Typing weak MSOL properties
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.
03
23
2017
3215
arXiv:1609.02753
10.23638/LMCS-13(1:14)2017
https://lmcs.episciences.org/3215