A constructive semantics for rewriting logic

We present an alternative model theory for rewriting logic in the calculus of inductive constructions. Making use of the Coq theorem proving environment, we create a formal specification of rewriting logic, and gain an interactive logical and semantic framework for rewriting logic, which is a logic well suited to the specification and validation of concurrent computations and proofs. We then show how we can use Coq and this specification as a formal proof environment for working with rewriting logic theories. Finally, we present tactics to automate portions of the proof generation and validation process.