Proving Operational Termination of Membership Equational Programs

Abstract : Reasoning about the termination of equational programs in sophisticated equational languages such as ELAN, MAUDE, OBJ, CAFEOBJ, HASKELL, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2008, 21 (1-2), pp.59-88
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00431474
Contributeur : Claude Marché <>
Soumis le : jeudi 12 novembre 2009 - 13:50:38
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 17 juin 2010 - 18:27:04

Fichier

duran08hosc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00431474, version 1

Collections

Citation

Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain. Proving Operational Termination of Membership Equational Programs. Higher-Order and Symbolic Computation, Springer Verlag, 2008, 21 (1-2), pp.59-88. 〈inria-00431474〉

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

120