A static higher-order dependency pair framework
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework.
The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | Program Analysis and Automated VerificationESOP at SUN II Chair(s): Stephanie Balzer Carnegie Mellon University | ||
10:30 30mTalk | Data-Races and Static Analysis for Interrupt-Driven Kernels ESOP Link to publication | ||
11:00 30mTalk | An abstract domain for trees with numeric relations ESOP Link to publication | ||
11:30 30mTalk | A static higher-order dependency pair framework ESOP Link to publication | ||
12:00 30mTalk | Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses ESOP Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK, Yue Li Heriot-Watt University, UK Link to publication |