Linear logic and linear types

In the world of programming languages, linear types are used to safely typecheck resource usage. A linear function f :: a %1 -> b pretends a is a resource, and must use it once (and only once) to make the result b. Linear types are the equivalent of linear logic from mathematics in computer science.

Some of the references I wanted to keep here:

• A taste of linear logic. Paper by Philip Wadler. Introduces linear logic in the context of programming.
• Stanford Encyclopedia of Philosophy, linear logic. Complete explanation of linear logic. Not an easy read.
• linear types GHC proposal
• linear-base library usage guide in Haskell. Provides basic functionality of linear types.
• linear-base in Hackage. Prelude.Linear and Data.Array.Mutable.Linear are of my interest.
• Linear types in stacktic-hs. I used linear types in my own library, which implements a stack-oriented language. Using linear resources turned out to be much easier in such kind of programming language.