Linearity in Higher-Order Recursion Schemes
Higher-order recursive schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of the lambda-Y-calculus and an extension of HORS, called linear HORS (LHORS).
First we prove that the two formalisms are equivalent and there exist polynomial-time translations between them. Then, in order to support model-checking of (trees generated by) LHORS, we propose a refined version of alternating parity tree automata, called LNAPTA, whose behaviour depends on information about linearity. We show that the complexity of LNAPTA model-checking for LHORS depends on two type-theoretic parameters: linear order and linear depth. The former is in general smaller than the standard notion of order and ignores linear function spaces. In contrast, the latter measures the depth of linear clusters inside a type. Our main result states that LNAPTA model-checking of LHORS of linear order n is n-EXPTIME-complete, when linear depth is fixed. This generalizes and improves upon the classic result of Ong, which relies on the standard notion of order.
To illustrate the significance of the result, we consider two applications: the MSO model-checking problem on variants of HORS with case distinction (RSFD and HORSC) on a finite domain and a call-by-value resource verification problem. In both cases, decidability can be established by translation into HORS, but the implied complexity bounds will be suboptimal due to increases in type order. In contrast, we show that the complexity bounds derived by translations into LHORS and appealing to our result are optimal in that they match the respective hardness results.
Thu 11 JanDisplayed time zone: Tijuana, Baja California change
13:40 - 15:20
Outside the boxResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
|Go with the Flow: Compositional Abstractions for Concurrent Data Structures|
Siddharth Krishna New York University, Dennis Shasha New York University, Thomas Wies New York University
|Parametricity versus the Universal Type|
Dominique Devriese KU Leuven, Marco Patrignani Saarland University, CISPA, Frank Piessens KU Leuven
|Linearity in Higher-Order Recursion Schemes|
Pierre Clairambault CNRS & ENS Lyon, Charles Grellois INRIA Sophia Antipolis & Aix-Marseille Université, Andrzej Murawski University of Oxford
|Symbolic Types for Lenient Symbolic Execution|
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Emina Torlak University of Washington