Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Typing Weak MSOL Properties
verfasst von : Sylvain Salvati, Igor Walukiewicz
Erschienen in: Foundations of Software Science and Computation Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.