Logique Et Interaction: Une Etude Semantique de La Totalite » książka
Logique Et Interaction: Une Etude Semantique de La Totalite
ISBN-13: 9786131510236 / Francuski / Miękka / 2010 / 288 str.
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."
Létude de langages de programmation toujours plus complexes requiert lemploi doutils mathématiques toujours plus sophistiqués. Lun de ces outils est la sémantique de jeux, qui propose de représenter les types par des jeux et les programmes par des stratégies. Si la technique a fait ses preuves pour de nombreux aspects des langages de programmation, elle a des difficultés à représenter les programmes totaux, se heurtant à des problèmes de terminaison similaires à ceux observés en théorie de la démonstration. Dans cette thèse, on étudie ces problèmes dans deux cas. Le premier est celui des jeux basés sur des arènes bien fondées : on donne un résultat général de terminaison des interactions, quon met en relation avec les théorèmes syntaxiques de normalisation. Le second correspond à certaines formules infinies, notamment inductives et co-inductives. On sinspire alors de conditions de gain utilisées en vérification pour construire un modèle précis dun langage de programmation total avec induction et co-induction.
Czytaj nas na:
KrainaKsiazek.PL - Księgarnia Internetowa
