ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 11:30 - 12:00 at SUN II - Program Analysis and Automated Verification Chair(s): Stephanie Balzer

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 Apr
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

esop-2019-papers
10:30 - 12:30: ESOP 2019 - Program Analysis and Automated Verification at SUN II
Chair(s): Stephanie BalzerCarnegie Mellon University
esop-2019-papers10:30 - 11:00
Talk
Link to publication
esop-2019-papers11:00 - 11:30
Talk
Matthieu Journault, Antoine MinéUPMC, France, Abdelraouf OuadjaoutSorbonne Université
Link to publication
esop-2019-papers11:30 - 12:00
Talk
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen
Link to publication
esop-2019-papers12:00 - 12:30
Talk
Henning BasoldCNRS & ENS Lyon, Ekaterina KomendantskayaHeriot-Watt University, UK, Yue LiHeriot-Watt University, UK
Link to publication