Cette thèse s'intéresse à la correspondance de Curry-Howard classique et son interaction avec le forcing de Cohen, en s'appuyant sur les outils de la réalisabilité classique. Dans une première partie, nous commençons par une introduction générale à la réalisabilité classique dans PA2, avec pour fil directeur l'extraction de témoin. Cette introduction couvre la description de la machine abstraite de Krivine (KAM), la construction des modèles, la réalisation de l'arithmétique et les deux principales problématiques calculatoires : la spécification et l'extraction de témoin. Pour illustrer la flexibilité de ce cadre, nous montrons ensuite qu'il s'adapte sans effort à diverses extensions : l'ajout d'instructions supplémentaires dans la KAM ou l'introduction de types de données primitifs tels que les entiers, les rationnels et les réels. Ces divers travaux ont été formalisés dans l'assistant de preuves Coq.Dans une seconde partie, nous redéfinissons ce cadre à l'ordre supérieur et le comparons à PA2. Ce changement, nécessaire pour exprimer pleinement la transformation de forcing, uniformise la théorie et permet d'intégrer tous les types de données. Nous présentons ensuite le forcing en réalisabilité classique, initialement dû à Krivine, puis l'étendons aux filtres génériques, lorsque les conditions de forcing forment un type de données. Cela permet de relire le forcing comme une transformation de programmes, dans le but d'obtenir des réalisateurs plus efficaces plutôt que des résultats d'indépendance. Cette méthode est illustrée notamment par l'exemple du théorème de Herbrand, dont la preuve par forcing donne un programme nettement plus efficace que la preuve habituelle. / This thesis focuses on the computational interpretation of Cohen's forcing through the classical Curry-Howard correspondence, using the tools of classical realizability. In a first part, we start by a general introduction to classical realizability in second-order arithmetic (PA2). We cover the description of the Krivine Abstract Machine (KAM), the construction of the realizability models, the realizers for arithmetic and the main two computational topics: specification and witness extraction. To illustrate the flexibility of this approach, we show that it can be effortlessly adapted to several extensions such as new instructions in the KAM or primitive datatypes like natural, rational and real numbers. These various works are formalized in the Coq proof assistant.In the second part, we redesign this framework in a higher-order setting and compare it to PA2.This change is necessary to fully express the forcing transformation, but it also allows us to uniformize the theory and integrate all datatypes. We present forcing in classical realizability, initially due to Krivine, and extend it to generic filters whenever the forcing conditions form a datatype. We can then see forcing as a program transformation adding a memory cell with its access primitives. Our aim is to find more efficient realizers rather than independence results, which are the common use of forcing techniques. The methodology is illustrated on the example of Herbrand's theorem, the proof by forcing of which gives a much more efficient program than the usual proof. Furthermore, we can recover the natural algorithm that one can write to solve the underlying computational problem if we use a datatype as forcing poset.
| Identifer | oai:union.ndltd.org:theses.fr/2014ENSL0915 |
| Date | 17 June 2014 |
| Creators | Rieg, Lionel |
| Contributors | Lyon, École normale supérieure, Miquel, Alexandre |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0021 seconds