Methods for Proving Termination of Rewriting-based Programming Languages by Transformation

Francisco Durán, Salvador Lucas, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)93-113
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume248
DOIs
StatePublished - Aug 5 2009

Keywords

  • Program Analysis and Verification
  • Rewriting Logic
  • Term Rewriting
  • Termination
  • Tools

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Methods for Proving Termination of Rewriting-based Programming Languages by Transformation'. Together they form a unique fingerprint.

Cite this