RT Conference Proceedings
T1 Theorem Proving for Maude Specifications Using Lean
A1 Rubio Cuéllar, Rubén Rafael
A1 Riesco Rodríguez, Adrián
A2 Riesco Rodríguez, Adrián
A2 Zhang, Min
AB 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.
SN 9783031172434
SN 9783031172441
SN 0302-9743
SN 1611-3349
YR 2022
FD 2022-10-10
LK https://hdl.handle.net/20.500.14352/94852
UL https://hdl.handle.net/20.500.14352/94852
LA eng
NO Agencia Estatal de Investigación
DS Docta Complutense
RD 26 dic 2025