Typing weak MSOL properties

TL;DR

This paper introduces a type system for lambda-Y-calculus that guarantees programs produce results satisfying specified weak MSOL properties, supported by a denotational semantics for soundness and completeness.

Contribution

It presents a novel type system linking lambda-Y-calculus execution results with weak MSOL properties, along with a denotational semantics for formal verification.

Findings

Type system ensures lambda-Y programs satisfy wMSOL properties

Denotational semantics proves soundness and completeness of the approach

Framework enables formal reasoning about program call trees

Abstract

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.