Maude2Lean: theorem proving for Maude specifications using Lean

DOI10.1016/J.JLAMP.2024.101005MaRDI QIDQ6643468zbMATH OpenFDO

Authors Rubén Rubio, Adrián Riesco

Publication date 26 November 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2024.101005

zbMATH Keywords

LeanMauderewriting logictheorem proving

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Maude: specification and programming in rewriting logic
• scientific article; zbMATH DE number 2043522
• Specification and proof in membership equational logic
• Strategies and user interfaces in Maude at work
• The Lean theorem prover (system description)

Cites work

• A constructor-based reachability logic for rewrite theories
• Abstract logical model checking of infinite-state systems using narrowing
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
• Black Ninjas in the dark: formal analysis of population protocols
• Conditional rewriting logic as a unified model of concurrency
• Equational formulas and pattern operations in initial order-sorted algebras
• Generalized rewrite theories, coherence completion, and symbolic methods
• Integrating Maude into Hets
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Logical foundations of CafeOBJ
• MTT: The Maude Termination Tool (System Description)
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Programming and symbolic computation in Maude
• Proof scores in the OTS/CafeOBJ method.
• Rewriting logic bibliography by topic: 1990--2011
• Rewriting modulo SMT and open system analysis
• Semantic foundations for generalized rewrite theories
• Specification and proof in membership equational logic
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• The Lean 4 theorem prover and programming language
• The Maude LTL model checker
• Twenty years of rewriting logic

Cited in

(2)

• DM-check: verifying invariants of concurrent systems by deductive model checking
• NuITP: accelerating the inductive verification of equational programs through symbolic simplification

This page was built for publication: Maude2Lean: theorem proving for Maude specifications using Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6643468)