Proving termination of membership equational programs

Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, Xavier Urbain

Research output: Contribution to conferencePaper

Abstract

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CAFEOBJ, MAUDE, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned tools.

Original languageEnglish (US)
Pages147-158
Number of pages12
DOIs
StatePublished - Jan 1 2004
EventProceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04 - Verona, Italy
Duration: Aug 24 2004Aug 25 2004

Other

OtherProceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04
CountryItaly
CityVerona
Period8/24/048/25/04

Keywords

  • Membership Equational Logic
  • Program Transformation
  • Term Rewriting
  • Termination

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Proving termination of membership equational programs'. Together they form a unique fingerprint.

  • Cite this

    Durán, F., Lucas, S., Meseguer, J., Marché, C., & Urbain, X. (2004). Proving termination of membership equational programs. 147-158. Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy. https://doi.org/10.1145/1014007.1014022