A detailed analysis of classical and intuitionistic sequential calculations enables us to design logics that are better adapted to the problems of computer science, and to develop, thanks to the Curry-Howard correspondence, intermediate formalisms between calculus and real programming languages.
The aim of this course is to give an overview of the motivations and applications of one of these logics, Linear Logic, which enables a finer analysis of demonstration and calculation processes, and to introduce the basic notions of the best-known intermediate calculations. The course will show how these two approaches converge, through appropriate computational interpretations.
The course pays particular attention to the syntactic and computational aspects of logical formalisms.