I read a lot about Linear Logic recently but I failed to find any real use to the logic.
I'd like to know how and where Linear Logic could be applied. Something like lambda calculus can be clearly used as a programming language (scheme, lisp). But I don't see how Linear Logic could be used in the real world...
On
In the context of programming language, there is the programming language that has multiple implementations. The syntax and the way it works is quite close to prolog. As it is pretty much a prototype, it lacks basic things such as sockets, reading file, debugger ...
This might be useful to anyone looking for code: http://www.lix.polytechnique.fr/~dale/lolli/
Secondly, in the "Related systems", there is the "Lolli for Alice" project that is quite interesting. It adds communication channels to Lolli. Using communication channels, it is possible to have 2 different process working altogether cooperatively.
There is an implementation of a planning system that makes it possible for 2 process to communicate with each others. Both process don't have to know the internals of the other to reach there goals and a predefined protocol of communication isn't necessary.
Using the resource semantic, it tries to find which action will make each agent reach there goal in parallel.
There for more information on the subject: http://dream.inf.ed.ac.uk/projects/dialoguell/
On
It matches Quantum Mechanics quite well, because the built-in conservation rules for propositions match the QM prohibitions on copying and deleting information:
"Physics, Topology, Logic and Computation: A Rosetta Stone"
John Baez, Mike Stay
http://math.ucr.edu/home/baez/rosetta.pdf
"Linear Logic for Generalized Quantum Mechanics"
Vaughn Pratt
http://boole.stanford.edu/pub/ql.pdf
These efforts are undertaken in a framework of Category Theory. The insight is that where intuitionist logics (Heyting algebras) correspond to cartesian closed categories (actually posets whose duals are also cartesian closed), linear logic corresponds to symmetric monoidal categories.
The fact that linear logic is resource-based, where propositions are supplied and consumed in inference rules, has the corollary that monoidal categories can be represented as 2D pictures with lines and boxes, where only free inputs and outputs can be left dangling (a la Feynman). Expressions are composed by connecting the wires on sub-expressions. The non-commutative aspects mean that spatial position and ordering of the wires is significant. If we introduce a 'crossing' operator, we have 'braided' monoidal categories, which are closely related to knot theory.
For much more on these diagrams, look at the beautifully illustrated papers from Bob Coecke et al. at Oxford.
Kat
Session types in type theory can be defined in terms of (intuitionistic) linear logic. See e.g. Caires and Pfenning. Whether or not you think session types (or even type theory) is a "real use" is up to you.
However, it is also used in practice as a language for for specifying properties which can then be verified to hold or not for a given model using model checking algorithms. See e.g. Faymonville and Zimmermann.