On discutera différentes manières de relier syntaxiquement la logique linéaire classique (LL) et sa version intuitionniste (ILL) : d'une part à travers la question de la conservativité de LL sur ILL (contre-exemples et conditions suffisantes), et d'autre part via l'étude de non-non traductions de LL dans ILL. On montrera que ces traductions permettent de représenter des extensions de LL dans ILL, mais aussi qu'elles peuvent être utilisées comme outil pour prouver des propriétés de LL : élimination des coupures et focalisation par exemple. Ces différents résultats ont été formalisés en Coq à l'aide de la bibliothèque Yalla, que nous présenterons brièvement.