Theorem Proving for Maude Specifications Using Lean

Abstract

Maude is a specification language based on rewriting logic whose programs can be executed, model checked, and analyzed with other techniques, but not easily theorem proved. On the other hand, Lean is a modern proof assistant based on the calculus of inductive constructions with a wide library of reusable proofs and definitions.

This paper presents a translation from the first formalism to the second, and a tool that derives a Lean program from a Maude module in a predictable way. Hence, theorems can be proved in Lean about Maude specifications.