Logique Et Interaction

L'tude de langages de programmation toujours plus complexes requiert l'emploi d'outils mathmatiques toujours plus sophistiqus. L'un de ces outils est la smantique de jeux, qui propose de reprsenter les types par des jeux et les programmes par des stratgies. Si la technique a fait ses preuves pour de nombreux aspects des langages de programmation, elle a des difficults reprsenter les programmes totaux, se heurtant des problmes de terminaison similaires ceux observs en thorie de la dmonstration. Dans cette thse, on tudie ces problmes dans deux cas. Le premier est celui des jeux bass sur des arnes bien fondes : on donne un rsultat gnral de terminaison des interactions, qu'on met en relation avec les thormes syntaxiques de normalisation. Le second correspond certaines formules infinies, notamment inductives et co-inductives. On s'inspire alors de conditions de gain utilises en vrification pour construire un modle prcis d'un langage de programmation total avec induction et co-induction.