Catalogue et commandes en ligne (paiement sécurisé, VISA ou MASTERCARD uniquement)

Revues disponibles par abonnement

Annales scientifiques de l'ENS

Astérisque

Bulletin de la SMF

Mémoires de la SMF

Revue d'Histoire des Mathématiques

Gazette des Mathématiciens

Séries de livres

Astérisque

Cours Spécialisés

Documents Mathématiques

Mémoires de la SMF

Panoramas et Synthèses

Séminaires et Congrès

Série Chaire Jean Morlet

SMF/AMS Texts and Monographs

La Série T

Fascicules « Journée Annuelle »

Autres livres

Donald E. Knuth - traductions françaises

Rééditions du Séminaire Nicolas Bourbaki

Rééditions des Œuvres de Jean Leray

Revue de l'Institut Elie Cartan

Editions électroniques

Annales scientifiques de l'ENS

Bulletin de la SMF

Revue d'Histoire des Mathématiques

Séminaires et Congrès

Plus d'information / Abonnement

Publications grand public

L'explosion des mathématiques (smf.emath.fr)

Mathématiques L'explosion continue (smf.emath.fr)

Zoom sur les métiers des maths (smf.emath.fr)

Zoom sur les métiers des mathématiques et de l'informatique (smf.emath.fr)

Où en sont les mathématiques ?

La Série T

Pour les auteurs

Soumission des manuscrits

Formats et documentation

Plus d'info

Liste de diffusion électronique (smf.emath.fr)

Information pour les libraires et diffuseurs (smf.emath.fr)

Publications de la SMF
fr en
Votre numéro IP : 54.197.150.255
Accès aux édit. élec. : SémCong

Panoramas et synthèses

Présentation de la publication

Texte de sollicitation pour les auteurs

Parutions

Dernières parutions

Comité de rédaction / Secrétariat

Volume :

Faire une recherche


Catalogue & commande

Panoramas et synthèses - Parutions - 27 (2009)

Parutions < 27

Interactive models of computation and program behaviour
Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, Paul-André Melliès
Panoramas et synthèses 27 (2009), xvi+275 pages
Acheter l'ouvrage
Sommaire

Résumé :
Modèles interactifs de calcul et de comportement de programme
Ce volume rassemble trois contributions portant sur le domaine logique et calcul et qui reflètent un courant actuel d'explicitation du contenu interactif des preuves et des programmes. Les trois chapitres peuvent être lus indépendamment et utilisent ou introduisent des outils fondamentaux du domaine: catégories, réalisabilité, machines abstraites. Un thème unificateur à travers l'ensemble du volume est celui des jeux et stratégies, qui transforme la correspondance entre preuves et programmes (connue sous le nom d'isomorphisme de Curry-Howard) en un triangle dont le troisième sommet met en valeur l'interaction et la dualité entre un programme et son contexte d'exécution, entre une preuve et des contre-preuves. L'introduction au volume place les contributions en perspective et offre une initiation rapide au lambda-calcul qui est et demeure l'épine dorsale de tout ce domaine de recherche.

Mots-clefs : Théorie de la démonstration, réalisabilité, machines abstraites, logique linéaire, sémantique des jeux

Abstract:
This volume contains three contributions in the field of logic and computation, that reflect current trends towards an interactive account of the meaning of proofs and programmes. The contributions can be read independently and use or introduce fundamental tools in the field: categories, realizability, abstract machines. Throughout the volume, a unifying theme is that of games and strategies, that turns the correspondance between proofs and programmes (the so-called Curry-Howard isomorphism) into a triangle whose third corner emphasizes interaction and duality between a program and its environement or between a proof and counter-proofs. The introduction to the volume places the contributions in perspective and provides a gentle beginner's introduction to the lambda-calculus, which is and remains the backbone of the whole field.

Keywords: Proof theory, realisability, abstract machines, linear logic, game semantics

Class. math. : 03F05, 03F52, 68Q55, 03B40, 03B70, 03G30, 68N18, 68N20


ISBN : 978-2-85629-273-0
ISSN : 1272-3835

Bibliographie:

73
Pierre-Louis Curien
Introduction to ``Interactive models of computation and program behaviour"
27 (2008) 1-7
74
Cousineau, G. and Curien, Pierre-Louis and Mauny, M.
The categorical abstract machine
Sci. Comput. Programming 8 (1987) 173–202
Math Reviews MR896255
Zentralblatt 634.68078
75
Curien, Pierre-Louis
Abstract Böhm trees
Math. Structures Comput. Sci. 8 (1998) 559–591
Math Reviews MR1672401
Zentralblatt 923.03021
76
Girard, Jean-Yves
Linear logic
Theoret. Comput. Sci. 50 (1987) 101
Math Reviews MR899269
Zentralblatt 629.03036
77
Kleene, S. C.
Realizability: a retrospective survey
in Cambridge Summer School in Mathematical Logic (Cambridge, 1971)
(1973) 95–112. Lecture Notes in Math., Vol. 337
Math Reviews MR0351775
Zentralblatt 272.02036
78
Krivine, J.-L.
A call-by-name lambda-calculus machine
Higher-Order and Symbolic Computation 20 (2007) 199–207