This article, the second in a series on logic in computer science, introduces linear logic and its applications. Linear logic, introduced by Girard in 1987, is characterized by its resource-conscious nature, distinguishing between static propositions in classical logic and dynamic properties or finite resources. The article highlights the differences between linear logic and classical and intuitionistic logics, emphasizing the absence of contraction and weakening rules. It explains the introduction of modal operators like ! (storage) and ? (non-storage) to manage resource reuse. The article provides an intuitive overview of linear logic, including its connectives (multiplicative and additive conjunctions, disjunctions, and negation), and discusses recent theoretical results. It also explores applications of linear logic in computer science, such as encoding Petri net reachability, functional programming, and natural language processing. The complexity of linear logic is examined, with key results including the undecidability of propositional linear logic and the PSPACE-completeness of certain fragments. Finally, the article outlines the sequent calculus rules for linear logic, detailing how these rules define the logic's structure and operations. The article concludes by summarizing the expressive power and practical applications of linear logic, highlighting its role in mainstream computer science.This article, the second in a series on logic in computer science, introduces linear logic and its applications. Linear logic, introduced by Girard in 1987, is characterized by its resource-conscious nature, distinguishing between static propositions in classical logic and dynamic properties or finite resources. The article highlights the differences between linear logic and classical and intuitionistic logics, emphasizing the absence of contraction and weakening rules. It explains the introduction of modal operators like ! (storage) and ? (non-storage) to manage resource reuse. The article provides an intuitive overview of linear logic, including its connectives (multiplicative and additive conjunctions, disjunctions, and negation), and discusses recent theoretical results. It also explores applications of linear logic in computer science, such as encoding Petri net reachability, functional programming, and natural language processing. The complexity of linear logic is examined, with key results including the undecidability of propositional linear logic and the PSPACE-completeness of certain fragments. Finally, the article outlines the sequent calculus rules for linear logic, detailing how these rules define the logic's structure and operations. The article concludes by summarizing the expressive power and practical applications of linear logic, highlighting its role in mainstream computer science.