Paper Info
Title
Proving termination of membership equational programs
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 muterm, 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.
Year
DOI
Venue
2004
10.1145/1014007.1014022
PEPM
Keywords
Field
DocType
expressive feature,equational program,equational subsets,maude equational program,proving termination,membership equational program,advanced typing,standard termination method,equational programming language,expressive equational program,termination tool,termination,programming language
Evaluation strategy,Programming language,Program transformation,Computer science,Correctness,Theoretical computer science,Equational programming
Conference
ISBN
Citations 
PageRank 
1-58113-835-0
28
1.29
References 
Authors
21
5
Name
Order
Citations
PageRank
Francisco Durán1281.29
Salvador Lucas21346.19
José Meseguer39533805.39
Claude Marché481447.43
Xavier Urbain528616.54