Advertisement
Published in:
2015 | OriginalPaper | Chapter
Typing Weak MSOL Properties
Authors : Sylvain Salvati, Igor Walukiewicz
Published in: Foundations of Software Science and Computation Structures
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We consider ł
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 (wMSO) is well suited to express properties of such trees. We give a type system for ensuring that the result of the execution of a
λY
-program satisfies a given wMSO property. In order to prove soundness and completeness of the system we construct a denotational semantics of
λY
-calculus that is capable of computing properties expressed in wMSO.