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
  • Consulter un extrait
  •  
                
  • Année : 2009
  • Tome : 27
  • Format : Électronique, 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.


Prix Papier
Price (paper only)
Prix public Public price 35.00 €
Prix membre Member price 25.00 €
Quantité
Quantity
- +


OPEN ACCESS
OPEN ACCESS

Grâce au soutien du CNRS, à votre générosité et à notre volonté de partager l'accès aux sciences, ce document est en libre accès. N'hésitez pas et continuez à nous soutenir !

Thanks to your generosity and our aim to promote access to science, this document has been made openly available. We expect you to be part of this project!