Maude2Lean: theorem proving for Maude specifications using Lean

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

Cites Work

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

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)