We discuss specific questions to be studied when formalizing linear logic and its meta-theory in a proof-assistant, and lessons to be taken from it. Among them we can mention:
* the structure of sequents, its relation with structural rules, and the role of permutations;
* the question of constructivity and its relation with the computational content of proofs;
* approaches to factorize results between variants of LL, including intuitionistic linear logic (double-negation translations, conservativity, generalized axioms);
* the representation of quantifiers, etc.
We focus on the specific choices to be done for developing a reusable library, and we will illustrate this through the Coq library Yalla: https://perso.ens-lyon.fr/olivier.laurent/yalla