Output details
11 - Computer Science and Informatics
University of Oxford
Output title
A type system equivalent to the modal Mu-calculus model checking of higher-order recursion schemes
Type
E - Conference contribution
Name of conference/published proceedings
Proceedings - Symposium on Logic in Computer Science
Volume number
-
Issue number
-
First page of article
179
ISSN of proceedings
1043-6871
Year of publication
2009
Number of additional authors
1
Additional information
<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.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
19
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
