  Linear logic was introduced by Jean-Yves Girard in his seminal work (Girard 1987).  While the origin of the discovery of this new logic comes from a semantical analysis of the models of System F (or polymorphic \(\lambda\)-calculus),  one can see the whole system of linear logic as a bold attempt to reconcile the beauty and symmetry of the systems for classical logic with the quest for constructive proofs that had led to intuitionistic logic.