Lionel Rieg (ENSIIE, Évry), L'interprétation calculatoire du forcing en réalisabilité classique : l'exemple des arbres de Herbrand

Programme

Résumé

Jean-Louis Krivine a présenté en 2011 une méthode pour combiner le forcing de Cohen et la réalisabilité classique dans laquelle les conditions de forcing s'interprètent calculatoirement comme des références non soumises aux backtracks. Alexandre Miquel a reformulé la traduction de programme sous-jacente dans un cadre typé, l'arithmétique d'ordre supérieur (PAω⁺) et l'a intégré directement à la KAM, donnant la KFAM (Krivine's Forcing Abstract Machine).

Dans cet exposé, je vais donner les idées essentielles de cette transformation de programme issue du forcing et expliquer comment elle peut s'utiliser en pratique. J'illustrerai ensuite cette méthodologie par un exemple concret : la construction d'arbre de Herbrand.