Maude2Lean: Theorem proving for Maude specifications using Lean

Thumbnail Image
Download
downoloadmaude2lean.pdf (782.73 KB)
Official URL
Full text at PDC
Publication date

2025

Authors
Advisors (or tutors)
Editors
Journal Title
Journal ISSN
Volume Title
Publisher
Elsevier
Citations
Google Scholar
Exportar
DC QDC MarcXML RDF MODS METS ORE-ATOM
URI
https://hdl.handle.net/20.500.14352/107912
Citation
Abstract
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.
Research Projects
Organizational Units
Journal Issue
Description
UCM subjects
Lógica simbólica y matemática (Matemáticas) , Lenguajes de programación
Unesco subjects
1102.03 Lógica Formal , 1203.23 Lenguajes de Programación
Keywords
Collections
Artículos