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:CCSD/oai:tel.archives-ouvertes.fr:tel-01061442 |
| Date | 17 June 2014 |
| Creators | Rieg, Lionel |
| Publisher | Ecole normale supérieure de lyon - ENS LYON |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0022 seconds