Output details
11 - Computer Science and Informatics
University of Oxford
A type system equivalent to the modal Mu-calculus model checking of higher-order recursion schemes
<11>
We give the first type-theoretic characterisation of the monadic-second-order (MSO) decidable theories of recursion schemes. Given a formula, we construct an intersection refinement type system in which a recursion scheme is typable if the tree it generates satisfies the formula, thus reducing the model checking problem to type checking. We show that the MSO model checking problem is fixed-parameter polytime in the size of the scheme. Our decision procedure is the basis of state-of-the-art higher-order model checkers (PREFACE and TRecS) which are the back-end engines of model checkers of functional programs.