← All papers
Formally Verified Insertion of Reference Counting Instructions
cs.LO
Jan 1, 2020 · v1
TL;DR
Implements and formally verifies a Lean 4 compiler pass for reference counting in Lean itself.
Abstract
This thesis presents a formally verified compiler pass for inserting reference counting instructions in Lean 4's intermediate representation. The correctness of the insertion algorithm is proved in Lean itself, ensuring that the resulting programs correctly manage memory through reference counting without introducing leaks or use-after-free errors.
Problem
Compiler passes for inserting reference counting instructions in functional language runtimes are complex and can introduce memory leaks or use-after-free errors if implemented incorrectly.
Approach
The thesis presents a formally verified compiler pass for inserting reference counting instructions in Lean 4 intermediate representation. The correctness of the insertion algorithm is proved in Lean itself, covering the guarantee that resulting programs manage memory correctly through reference counting.
Results
The verified compiler pass ensures that programs correctly manage memory without introducing leaks or use-after-free errors, with correctness guaranteed by machine-checked proofs in Lean.