, Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1, Logical Methods in Computer Science, vol.10, issue.4, 2010.
DOI : 10.2307/2269016
, Transfinite Update Procedures for Predicative Systems of Analysis, Proceedings of Computer Science Logic, 2011.
, Analysis of Learning in Peano Arithmetic, Annals of Pure and Applied Logic, 2011.
, A New Use of Friedman's Translation: Interactive Realizability, Festschrift of Helmut Schwichtenberg, Ontos-Verlag Series in Mathematical Logic
, Learning Based Realizability for HA + EM1 and 1-Backtracking Games: Soundness and Completeness, Annals of Pure and Applied Logic
, Interactive Realizability for Second-Order Heyting Arithmetic with EM 1 and SK 1 , preprint
, Update Procedures and the 1-Consistency of Arithmetic, MLQ, vol.30, issue.1, 2002.
DOI : 10.1002/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6
, A Symmetric Lambda-Calculus for Classical Program Extraction, Information and Computation, 1996.
, A New Approach to Program Extraction from Nonconstructive Proofs, ACM Transactions on Computational Logic, 2012.
, Classically and intuitionistically provably recursive functions, Lecture Notes in Mathematics, vol.669, pp.21-27, 1978.
DOI : 10.1007/BFb0103100
, Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes, Dialectica 12, pp.280-287, 1958.
, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, 1935.
DOI : 10.1007/BF01565428
, Proofs and Types, 1989.
, On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol.23, issue.02, 1962.
DOI : 10.1007/BF01447860
, Typed lambda-calculus in classical Zermelo-Fraenkel set theory, Archive for Mathematical Logic, 2001.
, Epsilon Substitution Method for Elementary Analysis, Archive for Mathematical Logic, 1996.
, Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 2006.