This project is a Lean port of Xavier Leroy's EUTypes 2019 summer school course on "Proving the correctness of a compiler". The original course material was written in Coq and demonstrates formal verification techniques for compiler correctness using a simple IMP language. This Lean implementation preserves the same theoretical foundations and proof structure while adapting the formalization to Lean's theorem proving system.
-
Notifications
You must be signed in to change notification settings - Fork 1
License
leanprover/LeroyCompilerVerificationCourse
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
No description, website, or topics provided.
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published