TY - JOUR
T1 - Methods for Proving Termination of Rewriting-based Programming Languages by Transformation
AU - Durán, Francisco
AU - Lucas, Salvador
AU - Meseguer, José
N1 - Funding Information:
1 Partially supported by the EU (FEDER) and Spanish MEC/MICINN under grants TIN2005-09405-C02-01 and TIN2008-03107. Email: duran@lcc.uma.es 2 Partially supported by the EU (FEDER) and the Spanish MEC/MICINN, under grant TIN 2007-68093-C02-02. Email: slucas@dsic.upv.es 3 Partially supported by ONR grant N00014-02-1-0715. Email: meseguer@cs.uiuc.edu
PY - 2009/8/5
Y1 - 2009/8/5
N2 - Despite the remarkable development of the theory of termination of rewriting, its application to high-level (rewriting-based) programming languages is far from being optimal. This is due to the need for features such as conditional equations and rules, types and subtypes, (possibly programmable) strategies for controlling the execution, matching modulo axioms, and so on, that are used in many programs and tend to place such programs outside the scope of current termination tools. The operational meaning of such features is often formalized in a proof theoretic manner by means of an inference system rather than just by a rewriting relation. The corresponding termination notions can also differ from the standard ones. During the last years we have introduced and implemented different notions and transformation techniques which have been proved useful for proving and disproving termination of such programs by using existing tools for proving termination of (variants of) rewriting. In this paper we provide an overview of our main contributions.
AB - Despite the remarkable development of the theory of termination of rewriting, its application to high-level (rewriting-based) programming languages is far from being optimal. This is due to the need for features such as conditional equations and rules, types and subtypes, (possibly programmable) strategies for controlling the execution, matching modulo axioms, and so on, that are used in many programs and tend to place such programs outside the scope of current termination tools. The operational meaning of such features is often formalized in a proof theoretic manner by means of an inference system rather than just by a rewriting relation. The corresponding termination notions can also differ from the standard ones. During the last years we have introduced and implemented different notions and transformation techniques which have been proved useful for proving and disproving termination of such programs by using existing tools for proving termination of (variants of) rewriting. In this paper we provide an overview of our main contributions.
KW - Program Analysis and Verification
KW - Rewriting Logic
KW - Term Rewriting
KW - Termination
KW - Tools
UR - http://www.scopus.com/inward/record.url?scp=68049127961&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=68049127961&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2009.07.062
DO - 10.1016/j.entcs.2009.07.062
M3 - Article
AN - SCOPUS:68049127961
SN - 1571-0661
VL - 248
SP - 93
EP - 113
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -