Skip to content

Commit

Permalink
Create README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem authored Sep 20, 2024
1 parent cb9da82 commit 0a5f992
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
# debruijn-ssa

This repository contains a formalization of SSA in Lean 4, along with it's equational semantics and a proof of completeness w.r.t an (otherwise unformalized) categorical semantics.

Unlike the related [`freyd-ssa`](github.com/imbrem/freyd-ssa), this version uses deBruijn indices rather than variable names, hence the repository name.

0 comments on commit 0a5f992

Please sign in to comment.