Soundness and Completeness are not enough: Linear Type Theories and Their Models Abstract: In this talk I will discuss the extension of the categorical Curry-Howard Isomorphism to Intuitionistic Linear Logic via three different type theories and their models. Investigation of the relationship between models will then show that more than soundness and completeness, categorical logicians interested in proofs *should* consider internal language results. Having these allows us to obtain precise relationships between models(systematization), as well as some simplification of the notions involved. (Joint work with Milly Maietti, Paola Maneggia and Eike Ritter)