Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update README: Add link to Lean tutorial, update ICFP 24 paper #408

Merged
merged 2 commits into from
Jan 6, 2025
Merged

Update README: Add link to Lean tutorial, update ICFP 24 paper #408

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1947c9e
Update README: Add link to Lean tutorial, update ICFP 24 paper
R1kM Jan 3, 2025
42c05a3
Remove obsolete link to base tutorial
R1kM Jan 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,9 @@ test`. Alternatively, call `REGEN_LLBC=1 make test-...` to regenerate only the n

If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html).

Additionally, a tutorial for using the Aeneas Lean backend is available [here](./tests/lean/Tutorial/); the original Rust file can be found [here](./tests/src/tutorial/src/lib.rs).
It requires a working installation of Lean.

## Usage

You should first generate the serialized `.llbc` file by calling Charon from *inside*
Expand Down Expand Up @@ -122,8 +125,6 @@ support for partial functions and extrinsic proofs of termination (see
and tactics specialized for monadic programs (see
`./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).

A (basic) tutorial for the Lean backend is available [here](./tests/lean/BaseTutorial.lean).

## Quick start for Nix users

Assuming Nix is installed, with a support for Flakes (`*`):
Expand All @@ -150,5 +151,4 @@ verification by functional
translation](https://dl.acm.org/doi/abs/10.1145/3547647)
([long version](https://arxiv.org/abs/2206.07185)). We also have a proof that
the symbolic execution performed by Aeneas during its translation correctly
implements a borrow checker, and published it in a
[preprint](https://arxiv.org/abs/2404.02680).
implements a borrow checker, and published it at ICFP 2024: [Sound Borrow-Checking for Rust via Symbolic Semantics](https://dl.acm.org/doi/10.1145/3674640) ([long version](https://arxiv.org/abs/2404.02680)).