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

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

Information légale