Maude2Lean: Theorem proving for Maude specifications using Lean

Simple item page
dc.contributor.authorRubio Cuéllar, Rubén Rafael
dc.contributor.authorRiesco Rodríguez, Adrián
dc.date.accessioned2024-09-04T14:42:56Z
dc.date.available2024-09-04T14:42:56Z
dc.date.issued2025-01
dc.description.abstractMaude 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.
dc.description.departmentDepto. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Informática
dc.description.fundingtypeAPC financiada por la UCM
dc.description.refereedTRUE
dc.description.sponsorshipAgencia Estatal de Investigación
dc.description.sponsorshipComunidad de Madrid
dc.description.statuspub
dc.identifier.doi10.1016/j.jlamp.2024.101005
dc.identifier.urihttps://hdl.handle.net/20.500.14352/107912
dc.journal.titleJournal of Logical and Algebraic Methods in Programming
dc.language.isoeng
dc.page.final22
dc.page.initial1
dc.publisherElsevier
dc.relation.projectIDinfo:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PID2019-108528RB-C22/ES/METODOS RIGUROSOS PARA EL DESARROLLO DE SISTEMAS SOFTWARE DE CALIDAD Y FIABILIDAD CERTIFICADAS/
dc.relation.projectIDinfo:eu-repo/grantAgreement/CAM//2018%2FTCS-4339//BLOQUES-CM
dc.rightsAttribution 4.0 Internationalen
dc.rights.accessRightsopen access
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/
dc.subject.keywordTheorem proving
dc.subject.keywordRewriting logic
dc.subject.keywordMaude
dc.subject.keywordLean
dc.subject.ucmLógica simbólica y matemática (Matemáticas)
dc.subject.ucmLenguajes de programación
dc.subject.unesco1102.03 Lógica Formal
dc.subject.unesco1203.23 Lenguajes de Programación
dc.titleMaude2Lean: Theorem proving for Maude specifications using Lean
dc.typejournal article
dc.type.hasVersionVoR
dc.volume.number142
dspace.entity.typePublication
relation.isAuthorOfPublication7dfd0267-1708-4f39-bda5-55a246b4bc41
relation.isAuthorOfPublication068dda11-d320-4634-a908-28a4bc4b0eb4
relation.isAuthorOfPublication.latestForDiscovery7dfd0267-1708-4f39-bda5-55a246b4bc41
Download
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
maude2lean.pdf
Size:
782.73 KB
Format:
Adobe Portable Document Format
downoload Download
Collections
Artículos