Phil Wadler has several "nice" papers about linear logics, e.g. this one: http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf http:/

Phil Wadler has several "nice" papers about linear logics, e.g. this one: http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/line... By nice I mean, nice if you are willing to deal papers about formal logic. Which excludes pretty much most people on this planet. But you asked. To put it in my own words, and bear in mind that the last time I've worked with linear logic was 15 years ago. A linear logic restricts how often you are allowed to use a proposition in a derviation or proof tree. The borrow checker is more like a linear type system. In linear type systems you restrict how often an identifier of a linear typed variable may be used. See, e.g. Phil Wadler's paper "Linear types can change the world", where he explores the idea to use linear types as an alternative to model the World(tm) in pure functional programming, i.e. an alternative to the IO monad.