From Linearity to Borrowing
summary
Builds a lightweight borrowing extension on a linear lambda calculus and implements the API as untyped terms validated by logic, not new runtime primitives. Proves type soundness of Borrow Calculus (BoCa) via a domain-specific separation logic Borrow Logic (BoLo), then proves the logic soundness in a semantic model that guarantees termination and leak freedom. Adds immutable borrows, lexical lifetimes, reborrowing and mutable borrows, and validates an implementation of withbar plus some unsafe-but-temporarily-correct code.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:26Linear references need borrowing
- 2:47Linear lambda calculus basics
- 4:11Immutable borrows in types
- 6:39Lifetime-based borrowing
- 8:25Separation logic for borrowing
- 11:11Model for references
- 13:59Termination and step indexing
- 14:40Summary
- 15:00Q&A
related talks
01h 22mCompile-Time Borrow Checker with Stateful Metaprogramming
28mBorrow checking Hylo
22mA Calculus of Inductive Linear Constructions
30mContinuations and Coexponentials
15mDenotational Recurrence Extraction for Amortized Analysis
19mType Inference Logics
31mIs there a use for linear types?
01h 04mLinear Haskell, Today and Tomorrow