-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
-program satisfies a given wMSO property. In order to prove soundness and completeness of the system we construct a denotational semantics of
-calculus that is capable of computing properties expressed in wMSO.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten