Readings in linear logic

This is a work in progress post outlining my research into linear logic and linear type systems.

Logic

Papers related directly to linear logic.

• Linear Logical Relations for Session-Based Concurrency Jorge A. Perez, Luıs Caires, Frank Pfenning, Bernardo Toninho 2012
• Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho 2009
• Linear logic, monads, and the lambda calculus Nick Benton, Philip Wadler 1996
• Structural Cut Elimination in Linear Logic Frank Pfenning 1994
• A taste of linear logic Philip Wadler 1993
• A syntax for linear logic Philip Wadler 1993
• There’s no substitute for linear logic Philip Wadler 1992
• Is there a use for linear logic? Philip Wadler 1991

Type Theory

Papers related to linear logic, specifically focusing on type theory.

• Once upon a type David N. Turner, Philip Wadler, Christian Mossin 1995
• Call-by-name, call-by-value, call-by-need, and the linear lambda calculus John Maraist, Martin Odersky, David Turner, Philip Wadler. 1995
• Linear types can change the world! Philip Wadler 1990

Courses

Online course materials related to linear logic.

• Oregon Programming Languages Summer School ‘13 Frank Pfenning 2013
• 15-816 Linear Logic at CMU Frank Pfenning 2012

Wikipedia & Web

Related wikipedia entries and other websites.

• Linear logic, Wikipedia
• Uniqueness type, Wikipedia
• Substructural type system, Wikipedia
• Linear Logic, Stanford Encyclopedia of Philosophy
• Linear Datatypes in ATS, Chris Double

Languages

Languages which support linear type systems.

• Rust Mozilla Research
• LinearML University of Nottingham
• Mercury University Of Melbourne
• ATS Hongwei Xi

I’m hoping to make this into a living document, so please submit pull requests or leave comments!