School Lectures
Wiki page of Linear Logic by Olivier Laurent: http://llwiki.enslyon.fr/
August, 27th (Monday)
9h10h30 
From CurryHoward correspondance to the geometrical turn in logic 
Joinet 
11h12h30 
From System F to the "coherent semantics" of LambdaCalculus 
Miquel 
14h3016h 
From linearity in coherent spaces to Linear Logic (sequent calculus) 
Vaux 
16h3018h 
Linear Logic: sequent calculus, polarities, focalization, phase semantics 
Beffara 
August, 28th (Tuesday)
9h10h30 
Pimentel 

11h12h30 
De Paiva 

14h3016h 
Fouqueré 

16h3018h 
Quatrini 
August, 29th (Wednesday)
9h10h30 
Melliès 

11h12h30 
Laurent 

14h3016h 
Laurent 

16h3018h 
From Proofnets to Geometry of Interaction 
Seiller 
August, 30th (Thursday)
8h9h30 
Girard 

10h11h30 
Geom. of interaction (2) 
Bagnol 
Lecturers
Lecturer 
Resumé 
Lecturer at university of Mediterranean (Marseille 2). Laboratory: Logic of programming (IML, University of Marseille 2 and CNRS). Main research areas: proof theory, linear logic, proofnets, geometry of interaction, quantum information, category theory, ludics, game semantics. 

Associated professor at University of Mediterranean (Marseille2). Laboratory: Logic of programming (IML, University of Marseille 2 and CNRS). Main research areas: logical foundations of interactive and non‐deterministic systems, linearalgebraic semantics of computation, proof/program correspondence outside functional computation. 

Mathematician and computer scientist, working in California, USA. Formerly a research scientist at the Intelligent Systems Laboratory of Palo Alto Research Center, California, and a search analyst for Cuill, Inc. in Menlo Park, CA. PhD in Mathematics from Cambridge University for work on "Dialectica Categories". She is Honorary Research Fellow at the School of computer science, University of Birmingham. Main research areas : logical approaches to computation, especially using Category Theory. 

Professor at the Computer sciences department of University Paris 13 (Paris Nord). Head of the Computer Sciences Laboratory of Paris Nord (LIPN)/ Member of the team: Logic, Computation, Resonning. Main research areas: Linear Logic. Computing theory and applications to linguistics. Ludics. Linear Logic. 

Researcher at CNRS. Laboratory of Informatics for Parallelism (ENSLyon and CNRS). Main research areas: proof theory, linear logic, polarized nets, differential nets, computational isomorphism, implicit computational complexity. 

Researcher at CNRS. Laboratory ProofsProgramsSystems, at the Department of mathematical sciences and Department of computer science. Main research areas: proof theory, game semantics, theory and practice of programming languages, formalized mathematics, proof assistants, mathematical physics, knot theory, quantum groups, ndimensionalalgebra,operads. 

Associated professor at University Denis Diderot (Paris 7). Currently at Laboratory of Informatics for Parallelism (ENSLyon and CNRS). Main research areas: proof theory, normalization, types systems, denotational semantics of proofs/programs, coherent semantics, subtyping, intuitionistic and classical realizability in set theory. 

Associated professor at Federal University of Minais Gerais and Univalle (Columbia). Department: mathematics. Main research areas: proof theory, linear logic, intersection types, lambdacalculus. 

Associated professor at University of Mediterranean (Marseille2). Laboratory: Logic of programming (IML, University of Marseille 2 and CNRS). Main research areas: proof theory, linear logic, denotational semantics, ludics and linguistic applications. 

Lecturer at University of Mediterranean (Marseille 2). Laboratory : Logic of programming (University of Marseille 2 and CNRS). Main research areas: proof theory, linear logic, ludics, geometry of interaction. 

Associated professor at University of Mediterranean (Marseille2). Laboratory : Logic of programming (IML, University of Marseille 2 and CNRS). Main research areas: proof theory, linear logic, denotational semantics, classical logic. 
Abstracts
Christophe FOUQUERÉ
Ludics: an introduction
Ludics is a rebuilding of Linear Logic from the sole concept of interaction on objects called designs, that abstract proofs. We introduce this formalism introduced around 2000 by J.Y. Girard, and in particular its main result, i.e. internal completeness results. We finish by presenting extensions of Ludics and in particular Cdesigns of K. Terui.