A suggestive game-theoretic interpretation of Gentzen's first consistency proof and a variation of Tait's sequent calculus. The process of cut-elimination was formulated as interaction of strategies, and a combinatorial lemma which expresses that this process terminates were proved.
(Together with S. Berardi and M. Bezem) A modified realizability interpretation of the system HAw with excluded middle and axiom of choices, with a (classical) proof of normalisation.
A general method, based on the use of topological model and formal topology, for interpreting in type theory objects whose existence rely usually on Zorn's lemma (prime ideals, non principal ultrafilters, valuation rings, ...) This method can be used also to interpret ``minimal bad sequence arguments''(Higman's lemma, Zantema's problem, ...) It can also be used to give new simple interpretations of logical systems in their intuitionistic version (like ID1 or Peano restricted to Sigma01-induction).
It has been argued (Weyl, Feferman) that excluded-middle may be justified over natural numbers, but that the ``openness'' of the notion of functions makes it less clear at the level of functions. Together with Erik Palmgren, we give a method to build constructively sheaf models that captures this intuition: these are models of the ``limited principle of omniscience'', while quantifications over functions is interpreted intuitionistically.