%0 Conference Paper
%A Rubio Cuéllar, Rubén Rafael
%A Riesco Rodríguez, Adrián
%T Theorem Proving for Maude Specifications Using Lean
%D 2022
%@ 0302-9743
%@ 1611-3349
%U https://hdl.handle.net/20.500.14352/94852
%X 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.
%~