Reflection and Strategies in Rewriting Logic Supported by Office of Naval Research Contracts N00014-95-C-0225 and N00014-96-C-0114, National Science Foundation Grant CCR-9224005, and by the Information Technology Promotion Agency, Japan, as a part of the Industrial Science and Technology Frontier Program "New Models for Software Architecture"

Manuel Clavel, José Mes eguer

Research output: Contribution to journalArticlepeer-review

Abstract

After giving general metalogical axioms characterizing reflection in general logics in terms of the notion of a universal theory, this paper specifies a finitely presented universal theory for rewriting logic and gives a detailed proof of the claim made in [5] that rewriting logic is reflective. The paper also gives general axioms for the notion of a strategy language internal to a given logic. Exploiting the fact that rewriting logic is reflexive, a general method for defining internal strategy languages for it and proving their correctness is proposed and is illustrated with an example. The Maude language has been used as an experimental vehicle for the exploration of these techniques. They seem quite promising for applications such as metaprogramming and module composition, logical framework representations, development of formal programming and proving environments, supercompilation, and formal verification of strategies.

Original languageEnglish (US)
Pages (from-to)126-148
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume4
Issue numberC
DOIs
StatePublished - 1996
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reflection and Strategies in Rewriting Logic Supported by Office of Naval Research Contracts N00014-95-C-0225 and N00014-96-C-0114, National Science Foundation Grant CCR-9224005, and by the Information Technology Promotion Agency, Japan, as a part of the Industrial Science and Technology Frontier Program "New Models for Software Architecture"'. Together they form a unique fingerprint.

Cite this