A new method for establishing conservativity of classical systems over their intuitionistic version
Thierry Coquand, Martin O. Hofmann · Mathematical Structures in Computer Science · 1999
We use a syntactical notion of Kripke models to obtain interpretations of subsystems of arithmetic in their intuitionistic counterparts. This yields, in particular, a new proof of Buss' result that the Skolem functions of Bounded Arithmetic are polynomial time computable.