https://github.com/dhsorens/lc3-lean
A proof system in Lean for LC-3
Science Score: 13.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
✓codemeta.json file
Found codemeta.json file -
○.zenodo.json file
-
○DOI references
-
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (4.1%) to scientific vocabulary
Last synced: 5 months ago
·
JSON representation
Repository
A proof system in Lean for LC-3
Statistics
- Stars: 0
- Watchers: 1
- Forks: 0
- Open Issues: 0
- Releases: 0
Created about 1 year ago
· Last pushed 11 months ago
Metadata Files
Readme
README.md
LC3-Lean
A proof system in Lean for LC3 Programs, following the article Write your Own Virtual Machine.
The purpose of this is to build formal verification tooling for a low-level Lean-based VM, in Lean.
Installation
Clone this repository and build the project.
lake build
This will give you a binary .lake/build/bin/lc3-lean
Run an assembled program, e.g. 2048:
.lake/build/bin/lc3-lean programs/2048.obj
If you add path-to-dir/.lake/build/bin/ to your PATH you can simply run
lc3-lean programs/2048.obj
Owner
- Name: Derek Sorensen
- Login: dhsorens
- Kind: user
- Location: Cambridge, UK
- Company: University of Cambridge
- Website: derekhsorensen.com
- Twitter: dhsorens
- Repositories: 1
- Profile: https://github.com/dhsorens
GitHub Events
Total
- Push event: 13
- Create event: 2
Last Year
- Push event: 13
- Create event: 2
Dependencies
.github/workflows/lean_action_ci.yml
actions
- actions/checkout v4 composite
- leanprover/lean-action v1 composite