Science Score: 57.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 4 DOI reference(s) in README -
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (6.8%) to scientific vocabulary
Keywords
Repository
Maude to Lean translator
Basic Info
- Host: GitHub
- Owner: fadoss
- License: gpl-3.0
- Language: Lean
- Default Branch: main
- Homepage: https://fadoss.github.io/maude2lean
- Size: 176 KB
Statistics
- Stars: 5
- Watchers: 1
- Forks: 0
- Open Issues: 0
- Releases: 1
Topics
Metadata Files
README.md
Maude to Lean translator
Translate Maude modules to Lean specifications where terms, sort membership, equational, and rewriting relations are defined inductively. Hence, theorems about Maude specifications can be proven in Lean.
The syntax of the tool is
$ maude2lean <Maude source or JSON/YAML/TOML file>+ [-o <output file>]
where the arguments are either a Maude file or a JSON, YAML, or TOML specification to customize the translation. The available options are documented in this JSON schema, and most of them can also be passed as command-line options (use --help for a list). Examples are available in the test directory.
The installation requirements for maude2lean are Python 3.9 and the maude Python library. Wheels and bundles are available in the releases section of this repository.
For a detailed description of the translation, see Maude2Lean: Theorem proving for Maude specifications using Lean or its shorter conference version.
Owner
- Name: FADoSS
- Login: fadoss
- Kind: organization
- Location: Madrid
- Website: https://maude.ucm.es/fadoss
- Repositories: 5
- Profile: https://github.com/fadoss
Formal Analysis and Design of Software Systems group (Universidad Complutense de Madrid)
Citation (CITATION.cff)
cff-version: 1.2.0
message: If you use this software, please cite it as below.
authors:
- family-names: Rubio
given-names: Rubén
orcid: https://orcid.org/0000-0003-2983-3404
- family-names: Riesco
given-names: Adrián
orcid: https://orcid.org/0000-0002-9716-4612
title: Maude to Lean translator
version: 1.0
date-released: 2022-10-14
url: https://github.com/fadoss/maude2lean
preferred-citation:
type: article
doi: 10.1016/j.jlamp.2024.101005
authors:
- family-names: Rubio
given-names: Rubén
orcid: https://orcid.org/0000-0003-2983-3404
- family-names: Riesco
given-names: Adrián
orcid: https://orcid.org/0000-0002-9716-4612
title: 'Maude2Lean: Theorem proving for Maude specifications using Lean'
journal: J. Log. Algebr. Methods Program.
year: 2024
month: 8
start: 1
end: 22
publisher:
name: Elsevier
references:
- type: conference-paper
doi: 10.1007/978-3-031-17244-1_16
authors:
- family-names: Rubio
given-names: Rubén
orcid: https://orcid.org/0000-0003-2983-3404
- family-names: Riesco
given-names: Adrián
orcid: https://orcid.org/0000-0002-9716-4612
title: Theorem Proving for Maude Specifications Using Lean
conference:
name: 23rd International Conference on Formal Engineering Methods (ICFEM) 2022
website: https://maude.ucm.es/ICFEM22/
date-start: 2022-10-24
date-end: 2022-10-27
year: 2022
month: 10
start: 263
end: 280
volume: 13478
collection-title: Lecture Notes in Computer Science
publisher:
name: Springer
GitHub Events
Total
- Watch event: 3
Last Year
- Watch event: 3