RT Journal Article
T1 Maude2Lean: Theorem proving for Maude specifications using Lean
A1 Rubio Cuéllar, Rubén Rafael
A1 Riesco Rodríguez, Adrián
AB Maude 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.
PB Elsevier
YR 2025
FD 2025-01
LK https://hdl.handle.net/20.500.14352/107912
UL https://hdl.handle.net/20.500.14352/107912
LA eng
NO Agencia Estatal de Investigación
NO Comunidad de Madrid
DS Docta Complutense
RD 6 oct 2024