Une dialectica matérialiste
Institution:
Sorbonne Paris CitéDisciplines:
Directors:
Abstract EN:
In this thesis, we show that the logical translation known as « dialectica » defined by Gödel in 1958 can be expressed in the Curry-Howard correspondance formalism, relating logical proofs to computer programs. In particular, it can be seen as a weak form of delimited control allowing to observe the use of free variables of a term through the stacks against which they are cut. We make this observation formal by simplifying Gödel's original translation, thanks to a linear reformulation due to De Paiva, and expressing it in the Krivine abstract machine. Such a simplification allows for an easy adaptation to the dependently-typed case. Quite a few variants are then defined and scrutinized. In addition, we give a presentation of the call-by-need reduction in a more canonical fashion, based on the use of a heterodox notion of contexts known as closure contexts.
Abstract FR:
Dans cette thèse, nous montrons que la traduction logique dite « dialectica » définie par Gödel en 1958 peut être exprimée dans le formalisme de la correspondance de Curry-Howard qui met en relation les preuves venant de la logique avec les programmes informatique. En particulier, on peut la voir comme une forme faible de contrôle délimité permettant d'observer l'utilisation des variables libres d'un terme par le biais des piles contre lesquelles elles se retrouvent coupées. Nous rendons cette constatation formelle en simplifiant la traduction originale de Gödel, grâce à une reformulation linéaire dûe à De Paiva, et en l'exprimant au travers de la machine de Krivine. La simplification de cette traduction permet en outre de l'adapter aisément au cas de la théorie des types dépendants. Un certain nombre de variantes sont en outre définies et étudiées. Par ailleurs, nous formulons une présentation de l'appel par nécessité dans un cadre plus canonique basé sur l'utilisation d'une notion de contexte hétérodoxe, appelés contextes de clôture.