Logique et interaction: une étude sémantique de la totalité Outils de sémantique de jeux pour la modélisation de systèmes logiques et langages de programmation totaux

L'etude de langages de programmation toujours plus complexes requiert l'emploi d'outils mathematiques toujours plus sophistiques. L'un de ces outils est la semantique de jeux, qui propose de representer les types par des jeux et les programmes par des strategies. Si la technique a fait ses preuves pour de nombreux aspects des langages de programmation, elle a des difficultes a representer les programmes totaux, se heurtant a des problemes de terminaison similaires a ceux observes en theorie de la demonstration. Dans cette these, on etudie ces problemes dans deux cas. Le premier est celui des jeux bases sur des arenes bien fondees: on donne un resultat general de terminaison des interactions, qu'on met en relation avec les theoremes syntaxiques de normalisation. Le second correspond a certaines formules infinies, notamment inductives et co-inductives. On s'inspire alors de conditions de gain utilisees en verification pour construire un modele precis d'un langage de programmation total avec induction et co-induction."