SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Reflection and Strategies in Rewriting Logic
 by Manuel Clavel, Francisco Duran & Josť Meseguer.

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 [6] 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.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy