This is a full mechanization of the From Linearity to Borrowing paper in Lean https://dl.acm.org/doi/10.1145/3764117

The work was almost entirely done by Claude over the course of 3-4 weeks. It follows the paper and technical supplement as closely as I could and nearly every definition and lemma in the paper is covered, including the Fundamental Property and Adequacy (all well typed programs terminate with an empty heap, essentially).

The original paper is not mine and I have no connection with the authors, this was just a spare time project while I try and learn language design.