Output details
11 - Computer Science and Informatics
University of Oxford
Return to search
Output 0 of 0 in the submission
Output title
Verifying higher-order functional programs with pattern-matching algebraic data types
Type
E - Conference contribution
Name of conference/published proceedings
Conference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume number
-
Issue number
-
First page of article
587
ISSN of proceedings
0730-8566
Year of publication
2011
Number of additional authors
1
Additional information
<11>
The inability of recursion schemes to model pattern-matching algebraic data types limits the impact of higher-order model checking, because pattern-matching is ubiquitous in functional programming. We introduce Pattern-Matching Recursion Schemes (PMRS)---essentially the GHC Core---to repair this deficiency. We present a semi-algorithm for the (undecidable) PMRS verification problem: given property Phi, PMRS P and regular input set I, does every term reachable from I under rewriting by P satisfy Phi? Based on model-checking and counterexample guided abstraction refinement, our method is sound and guaranteed to return a counter-example for no-instances.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
2
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
