When I was a master's student in Paris I was exposed to the following standard narrative: "J.-Y. Girard invented coherence spaces, then he noticed the decomposition $A \to B~=~!A \multimap B$ and that's how linear logic was born". But I've come across some conflicting information:
some people who have known Girard personally told me that he invented the normal functor / power series semantics of the λ-calculus first, and that's where he actually discovered linearity (corresponding to degree 1 monomials);
on the other hand, Girard's written quotes seem to indicate that linear logic indeed comes from coherence spaces, not from the interpretation of function types but from that of intuitionistic sum types as $A + B~=~!A \oplus !B$:
Linear logic first appeared after the author had been challenged by Berry and Curien to extend the coherent semantics (at the time: qualitative semantics) to the sum of types
(From Linear Logic (1987) section V)
It is this decomposition which is the origin of linear logic: the operations ⊕ (direct sum) and ! (linearisation) are in fact logical operations in their own right.
(From Proofs and Types chapter 12)
So what is the actual story here? (Is there any way to know?)
