| Identifiant de l'article : |
 |
tel-00460805, version 1 |
|
|
| titre : |
|
Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire |
|
|
| auteur(s) : |
|
Olivier Laurent1 |
|
|
| laboratoire : |
|
| 1 : |
LIP - Laboratoire de l'Informatique du Parallélisme |
|
|
|
| Équipe de recherche : |
|
Plume |
| résumé : |
|
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. |
|
|
| domaine : |
|
Mathématiques
|
|
|
|
| langue : |
|
Français |
|
|
|
| mots-clés : |
|
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 |
|
|
| date de soutenance : |
|
05/02/2010 |
|
|
| organisme de délivrance : |
|
Université Paris-Diderot - Paris VII |
|
|
| président du jury : |
|
Jean Goubault-Larrecq |
|
|
| composition du Jury : |
|
Pierre-Louis Curien (rapporteur)
Jean-Yves Girard
Gordon Plotkin
Peter Selinger (rapporteur)
Glynn Winskel (rapporteur) |
|
|
Récupérer au format
