Titre : | Interactive models of computation and program behaviour | Type de document : | texte imprimé | Editeur : | Paris : Société Mathématique de France | Année de publication : | 2009 | Collection : | Panoramas et Synthèses, ISSN 1272-3835 num. 27 | Importance : | XVI-275 p. | Présentation : | ill. | ISBN/ISSN/EAN : | 978-2-85629-273-0 | Langues : | Anglais (eng) | Mots-clés : | théorie de la démonstration réalisabilité machine abstraite ogique linéaire sémantique des jeux | Résumé : | 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. | Note de contenu : | références |
Interactive models of computation and program behaviour [texte imprimé] . - Société Mathématique de France, 2009 . - XVI-275 p. : ill.. - ( Panoramas et Synthèses, ISSN 1272-3835; 27) . ISBN : 978-2-85629-273-0 Langues : Anglais ( eng) Mots-clés : | théorie de la démonstration réalisabilité machine abstraite ogique linéaire sémantique des jeux | Résumé : | 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. | Note de contenu : | références |
| |