Une analyse fine des calculs de séquents classiques et intuitionnistes permet de concevoir des logiques plus adaptées aux problèmes de l'informatique et de dévélopper, grâce à la correspondance de Curry-Howard des formalismes intermédiaires entre le λ-calcul et les vrais langages de programmation.
Ce cours a pour but de donner une vision d'ensemble des motivations et des applications d'une de ces logiques, la Logique Linéaire, qui permet une analyse plus fine des processus de démonstration et de calcul, et d'introduire les notions de base des calculs intermédiaires les plus connus. On montrera dans le cours comment ces deux approches se rejoignent, à travers des interprétations calculatoires adaptées.
Ce cours dédie une attention toute particulière aux aspects syntaxiques et calculatoires des formalismes logiques.
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.