Partial formalisation for the proof of well-typedness of the reference counting algorithm/compiler in Counting Immutable Beans (https://arxiv.org/abs/1908.05647) using Lean 3 for my BSc thesis. The full thesis ("Formally Verified Insertion of Reference Counting Instructions") can be found at https://pp.ipd.kit.edu/publication.php?id=huisinga19bachelorarbeit.
mhuisi/rc-correctness
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|