School Lectures

Wiki page of Linear Logic by Olivier Laurent: http://llwiki.ens-lyon.fr/

August, 27th (Monday)

9h-10h30

From Curry-Howard correspondance to the geometrical turn in logic

Joinet

11h-12h30

From System F to the "coherent semantics" of Lambda-Calculus

Miquel

14h30-16h

From linearity in coherent spaces to Linear Logic (sequent calculus)

Vaux

16h30-18h

Linear Logic: sequent calculus, polarities, focalization, phase semantics

Beffara

August, 28th (Tuesday)

9h-10h30

Linear Logic with subexponentials

Pimentel

11h-12h30

Game semantics

De Paiva

14h30-16h

Ludics: an introduction

Fouqueré

16h30-18h

Classical logic: LC, correlations spaces

Quatrini

August, 29th (Wednesday)

9h-10h30

MLL Proof nets. Sequentialization. Normalization.

Melliès

11h-12h30

MELL Proof nets. Polarized nets.

Laurent

14h30-16h

Light Logics

Laurent

16h30-18h

From Proof-nets to Geometry of Interaction

Seiller

August, 30th (Thursday)

8h-9h30

Geom. of interaction (1)

Girard

10h-11h30

Geom. of interaction (2)

Bagnol

Lecturers

Lecturer

Resumé

Marc BAGNOL

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.

Emmanuel BEFFARA

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, linear-algebraic semantics of computation, proof/program correspondence outside functional computation.

Valeria DE PAIVA

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.

Christophe FOUQUERÉ

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.

Olivier LAURENT

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

Paul-André MELLIÈS

Researcher at CNRS. Laboratory Proofs-Programs-Systems, 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.

Alexandre MIQUEL

Associated professor at University Denis Diderot (Paris 7). Currently at Laboratory of Informatics for Parallelism (ENS-Lyon 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.

Elaine PIMENTEL

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

Myriam QUATRINI

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.

Thomas SEILLER

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.

Lionel VAUX

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 C-designs of K. Terui.

TecMF: ProofTheory2012/SchoolLectures (last edited 2012-09-04 10:42:03 by BrunoLopes)