Description

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.

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 isomor-phism) 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.