Rubio Cuéllar, Rubén RafaelRiesco Rodríguez, AdriánRiesco Rodríguez, AdriánZhang, Min2024-01-232024-01-232022-10-10978303117243497830311724410302-97431611-334910.1007/978-3-031-17244-1_16https://hdl.handle.net/20.500.14352/94852Maude 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.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/conference paperopen accessTheorem provingRewriting logicMaudeLeanLenguajes de programaciónLógica simbólica y matemática (Matemáticas)1203.23 Lenguajes de Programación1102.03 Lógica Formal