No-counterexample interpretation et spécification des théorèmes de l'arithmétique

Denis Bonnay

This paper presents two different ways of extracting the computational content of formal proofs in arithmetic. The first one corresponds to Kreisel's No-counterexample Interpretati…