Simple lambda lifting: Formalisation in Lean and a new efficient algorithm

Abstract

Lambda lifting is a technique used in compilers to convert nested function definitions to top-level function definitions. A series of papers has led to an 𝑂(𝑛2) algorithm, however it is complex. We present a simple 𝑂(𝑛2) algorithm for lambda lifting and prove its correctness. We also formalise a lambda lifting specification from the literature in Lean 4, and use that to prove some of the properties and test our algorithm on generated test cases. One of our contributions is to formalise the notion of a “complete” and “minimal” lifting, addressing a small issue with the handling of unused functions that to our knowledge affects all previous algorithms.