SMF

Modèles interactifs de calcul et de comportement de programme

Interactive models of computation and program behaviour

Pierre-Louis CURIEN, Hugo HERBELIN, Jean-Louis KRIVINE, Paul-André MELLIÈS
Modèles interactifs de calcul et de comportement de programme
  • Année : 2009
  • Tome : 27
  • Format : Papier
  • Langue de l'ouvrage :
    Anglais
  • Class. Math. : 03F05, 03F52, 68Q55, 03B40, 03B70, 03G30, 68N18, 68N20
  • Nb. de pages : xvi+275
  • ISBN : 978-2-85629-273-0
  • ISSN : 1272-3835

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 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.

Théorie de la démonstration, réalisabilité, machines abstraites, logique linéaire, sémantique des jeux
Proof theory, realisability, abstract machines, linear logic, game semantics
Prix
Adhérent 21 €
Non-Adhérent 30 €
Quantité
- +