Skip to content

Commit

Permalink
Slightly tune readme
Browse files Browse the repository at this point in the history
  • Loading branch information
Kiiyya committed Jan 10, 2025
1 parent f8b8ab6 commit 1170da0
Showing 1 changed file with 2 additions and 9 deletions.
11 changes: 2 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,4 @@
# Embedding of Boogie into Lean

## Interaction Trees
Allow us to model:
- Non-termination
- Memory, potentially even with weaker guarantees
- Assume, Assert, Non-determinism
- (Mutual) Recursion
- Async?
- External APIs?

We use interaction trees in order to represent imperative programs.
Currently this is a shallow embedding, with a Boogie DSL elaborating directly to ITrees.

0 comments on commit 1170da0

Please sign in to comment.