Realizability methods allowed to prove normalization results on many typed calculi.
Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic.
Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources).
Anchored within the realizability framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using realizability) come for free.
J'ai effectué ma thèse sous la direction de Thomas Ehrhard dans le laboratoire PPS (Preuves Programmes Systèmes). Le sujet tourne autour du λ-calcul différentiel, de la logique linéaire et des réseaux d'interaction. Vous trouverez ici un résumé et mon mémoire.
J'ai effectué différents stage de recherche lors de mes études. Vous trouverez ici mes rapports de stage (algèbres de processus, λ-calcul, logique, preuves, calcul quantique).
J'ai été élève de l'ENS Lyon. J'ai suivi les deux premières années du cursus Informatique. Je suis ensuite allé étudier à Paris en 2ème année du MPRI (Mastère Parisien de Recherche en Informatique).
Voici la liste des cours que j'ai suivi.