Cette thèse étudie différents aspects de la réalisabilité classique due à Jean-Louis Krivine. Celle-ci permet de mettre en oeuvre l'isomorphisme de Curry-Howard: on peut ainsi associer un programme à chaque démonstration mathématique, et considérer chaque théorème comme une spécification. Dans un premier temps, on rappelle le formalisme de la réalisabilité classique ainsi que certains de ses résultats fondamentaux. On s'attache ensuite à l'analyse des contenus opérationnels obtenus suivant deux méthodes différentes d'étude des entiers des modèles de la réalisabilité. Dans un second temps, on rappelle la notion de jeu qui peut être associée à chaque formule du premier ordre dans ce cadre. Ces jeux permettent d'établir une correspondance entre les formules valides du calcul des prédicats et les protocoles de la couche transport des réseaux, que l'on peut spécifier de manière claire et précise par ce biais. La dernière partie est consacrée à l'étude de l'axiome du choix dépendant. On montre que la méthode développée pour le réaliser s'adapte à une expression simple de celui-ci au niveau des individus d'un modèle. On utilise enfin l'instruction associée pour réaliser un cas particulier du théorème de Herbrand. Le terme obtenu effectue une opération très générale, qui peut être interprétée dans le cadre des protocoles réseaux.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00293688 |
| Date | 17 July 2008 |
| Creators | Hesse, Philippe |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds