Original Summary

This is a full proof of the From Linearity to Borrowing paper in Lean <a href="https:&#x2F;&#x2F;dl.acm.org&#x2F;doi&#x2F;10.1145&#x2F;3764117" rel="nofollow">https:&#x2F;&#x2F;dl.acm.org&#x2F;doi&#x2F;10.1145&#x2F;3764117</a><p>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).<p>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.

  • 情报分类：技术学习与提效
  • 分类依据：内容涉及技术、AI、软件工具或工程实践
  • 信息来源：Hacker News 新项目
  • 发布时间：2026/10/3 03:56:51