CIRM - HOME (EN)
CIRM - ACCUEIL (FR)

Picture

6 videos available for this event!
HYBRID RESEARCH SCHOOL – ECOLE DE RECHERCHE

Linear Logic Winter School
École d’hiver de logique linéaire

​24 – 28 January 2022

Scientific Committee
Comité scientifique

Thomas Ehrhard (CNRS, Université de Paris)
Claudia Faggian (CNRS, Université de Paris)
Olivier Laurent (CNRS, ENS Lyon)
Laurent Regnier (Université d’Aix-Marseille)
Lorenzo Tortora de Falco (Roma Tre University)
Lionel Vaux Auclair (Université d’Aix-Marseille)
Organizing Committee
Comité d’organisation

Lorenzo Tortora de Falco (Roma Tre University)
Lionel Vaux Auclair (Université d’Aix-Marseille)
Description
The rôle Linear Logic as an underlying structure of logic and computation is
widely acknowledged. As such, it is not only a research subject in itself, but
also a conceptual framework, offering an original and fruitful viewpoint on the objects of logic and computer science.

This school will offer an introduction to the main concepts and essential
results in Linear Logic, based on an undergoing project to produce a reference textbook, within the International Research Network on Linear Logic. The lectures will be given by some of the foremost experts of the subject, involved in that collaborative effort. The school will moreover include a lab work session, using recently developed software to construct and manipulate Linear Logic proofs.

In addition to the lectures, the week will be concluded by a series of tutorial
talks on a selection of advanced subjects, reflecting current research
directions involving Linear Logic.
Le rôle de la Logique Linéaire comme structure sous-jacente de la logique et du calcul est largement reconnu. En tant que telle, elle constitue non seulement un sujet de recherche en elle-même, mais aussi un cadre conceptuel, qui offre un point de vue original et fructueux sur les objets de la logique et de l’informatique.

Cette école proposera une introduction aux principaux concepts et résultats de la Logique Linéaire, sur la base d’un livre de cours, actuellement en cours de rédaction au sein du Réseau de recherche international en Logique Linéaire. Les cours seront donnés par certains des meilleurs experts du domaine, impliqués dans cet effort collaboratif. L’école comprendra également une session de travaux pratiques, à l’aide de logiciels récemment développés, permettant de construire et manipuler des preuves de Logique Linéaire.

À la suite des cours, la semaine se concluera par une série d’exposés, toujours sur un mode introductif, abordant une sélection de sujets avancés, reflétant les thèmes de recherche actuels nourris par la Logique Linéaire.
Speakers 

Beniamino Accatoli (LIX, École Polytechnique)    Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic                                                             
Thomas Ehrhard (CNRS, Université de Paris) & Laurent Regnier (Université d’Aix-Marseille)   Introduction, part I: from Hilbert’s program to Linear Logic, via the Curry-Howard isomorphism, part II: some fruits of Linear Logic
Jean-Yves Girard (I2M, Aix-Marseille)   Deux ou trois choses que je sais d’elle : la logique (in French, with English subtitles)                                                                              Marie Kerjean (LIPN, Paris 13)    Differential Linear Logic extended to Differential Operators                                                                                                                  
Olivier Laurent (LIP, ÉNS Lyon)    Multiplicative proof nets, part I: a graphical syntax for proofs – Multiplicative proof nets, part II: back to sequent calculus                        Giulio Manzonetto (LIPN, Paris 13)    Taylor expansion, at work                                                                                                             
Damiano Mazza (LIPN, Paris 13)    Heterodox Exponential Modalities in Linear Logic                                                                                                                  
Paul-André Melliès (IRIF, Sorbonne)    Categorical models                                                                                                            
Dale Miller (LIX, École Polytechnique)    Focused proof systems                                                                                                      
Koko Muroya (KURIMS, Kyoto)    Program semantics with token passing                                                                                                                    
Michele Pagani (IRIF, Paris) Sequent Calculus, part I: formulas and rules
Alexis Saurin (IRIF, Paris)    Sequent Calculus, part II: Cut elimination                                          
Christine Tasson (LiP6, Paris)    The relational model of Linear Logic                                                                                                                  
Lorenzo Tortora de Falco (Roma Tre University)  MELL proof nets, part 2: a proof of strong normalization
Lionel Vaux Auclair (I2M, Aix-Marseille)    MELL proof nets, part 1: definitions, properties, and translation of λ-calculus                          

SPONSORS