Modèles interactifs de calcul et de comportement de programme
Interactive models of computation and program behaviour
Anglais
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.
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 !