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.
CITATION STYLE
Salvati, S., & Walukiewicz, I. (2015). Typing weak MSOL properties. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9034, pp. 343–357). Springer Verlag. https://doi.org/10.1007/978-3-662-46678-0_22
Mendeley helps you to discover research relevant for your work.