Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire

Olivier Laurent

tel-00460805, version 1

Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire

Olivier Laurent () ¹

Université Paris-Diderot - Paris VII (05/02/2010), Jean Goubault-Larrecq (Pr.)

Abstract: La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.

1: Laboratoire de l'Informatique du Parallélisme (LIP)
Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I

tel-00460805, version 1
http://tel.archives-ouvertes.fr/tel-00460805
oai:tel.archives-ouvertes.fr:tel-00460805
From: Olivier Laurent <>
Submitted on: Tuesday, 2 March 2010 15:17:03
Updated on: Thursday, 6 May 2010 11:36:24

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

%F tel-00460805, version 1
%0 Thesis
%U http://tel.archives-ouvertes.fr/tel-00460805
%T Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire
%A Laurent, Olivier
%+ Laboratoire de l'Informatique du Parallélisme - LIP
%8 2010-02-05
%X La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.
%X Linear Logic is now part of the toolbox for the development of proof theory as well as for the study of the Curry-Howard correspondence. We present here three important directions for the application of methods coming from linear logic: * proof theory for classical logic and its computational aspects using game semantics mainly; * implicit computational complexity by means of the denotational models of light linear logic systems; * concurrency theory and its logical foundations through the new ingredients provided by differential linear logic. Linear Logic provides us this way with a common framework for the study of various logical aspects of computation.
%2 MATH
%I Université Paris-Diderot - Paris VII
%G French
%Z Jean Goubault-Larrecq
%Z Pierre-Louis Curien (rapporteur) Jean-Yves Girard Gordon Plotkin Peter Selinger (rapporteur) Glynn Winskel (rapporteur)
%K logique linéaire ; théorie de la démonstration ; correspondance de Curry-Howard ; logique classique ; lambda-calcul ; sémantique des jeux ; complexité implicite ; concurrence ; pi-calcul ; logique linéaire différentielle ; réseaux d'interaction