Rubio Cuéllar, Rubén RafaelRiesco Rodríguez, Adrián2024-09-042024-09-042024-0110.1016/j.jlamp.2024.101005https://hdl.handle.net/20.500.14352/107912Maude is a specification language based on rewriting logic whose programs can be executed, model checked, and analyzed with other automated 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 the maude2lean tool that predictably derives a Lean program from a Maude module. Hence, theorems can be proved in Lean about Maude specifications.engAttribution 4.0 Internationalhttp://creativecommons.org/licenses/by/4.0/journal articleopen accessTheorem provingRewriting logicMaudeLeanLógica simbólica y matemática (Matemáticas)Lenguajes de programación1102.03 Lógica Formal1203.23 Lenguajes de Programación