Linear Logic, what is it used for? 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...

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
