Show HN: A lean formalization of From Linearity to Borrowing

Category: other

Tags: formal-verification, lean4, programming-languages, linear-types, borrowing, mechanized-proof

Score: 6.0/10 (Innovation: 6, Technical: 8, Documentation: 7, Utility: 3)

A Lean 4 formalization of the paper 'From Linearity to Borrowing', mechanizing its definitions, proofs, and main results including the Fundamental Property and adequacy. It provides a verified trust base for the theory of borrowing in linear type systems, with a comparator challenge to independently check the proof.

Target audience: programming languages researchers, formal methods researchers, type system theorists

Repository: https://github.com/empath-nirvana/bolo-formalization · Lean · 1 stars

View on Hacker News