formally verified language

We formally define a language and prove its memory safety properties.

report/ - specification and project report (pdf)
paper-review/ - review of the background paper used for this project (pdf, paper link)
presentation/ - presentation of the project (pdf)
lang/ - implementation and proofs in Scala using Stainless
lean/ - implementation and proofs in Lean

Name		Name	Last commit message	Last commit date
Latest commit History 101 Commits
.github/workflows		.github/workflows
lang		lang
lean		lean
paper-review		paper-review
presentation		presentation
report		report
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md

Provide feedback