1. Ulrich Berger (2005): Uniform Heyting Arithmetic.. Ann. Pure Appl. Logic 133(1–3), pp. 125–148. Available at
  2. Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg (2002): Refined program extraction form classical proofs.. Ann. Pure Appl. Logic 114(1–3), pp. 3–25.
  3. Matthias Felleisen & Daniel P. Friedman (1989): A Syntactic Theory of Sequential State. Theor. Comput. Sci. 69(3), pp. 243–287.
  4. Harvey Friedman (1978): Classically and intuitionistically provably recursive functions. Lecture Notes in Mathematics 669, pp. 21–27.
  5. Kurt Gödel (1958): Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, pp. 280–287.
  6. Timothy Griffin (1990): A Formulae-as-Types Notion of Control. In: POPL, pp. 47–58. Available at
  7. Mircea-Dan Hernest (2007): Optimized programs from (non-constructive) proofs by the light (monotone) Dialectica interpretation. Ph.D. thesis. Ecole Polytechnique. Available at
  8. Mircea-Dan Hernest & Trifon Trifonov (2010): Light Dialectica Revisited. Annals of Pure and Applied Logic 161(11), pp. 1313–1430. Available at
  9. Ulrich Kohlenbach (2008): Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer. Available at
  10. Yevgeniy Makarov (2006): Practical Program Extraction from Classical Proofs. Electr. Notes Theor. Comput. Sci. 155, pp. 521–542. Available at
  11. Michel Parigot (1992): λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Andrei Voronkov: LPAR, Lecture Notes in Computer Science 624. Springer, pp. 190–201. Available at
  12. Diana Ratiu & Helmut Schwichtenberg (2009): Decorating Proofs. To appear in Mints Festschrift, draft at: schwicht/papers/mints09/deco20090728.pdf.
  13. Diana Ratiu & Trifon Trifonov (2009): Exploring the Computational Content of the Infinite Pigeonhole Principle. Draft at trifonov/papers/iph.pdf. Available at To appear in Proceedings of CiE 2008, Journal of Logic and Computation.
  14. Helmut Schwichtenberg (2008): Dialectica interpretation of well-founded induction. Mathematical Logic Quarterly 54(3), pp. 229–239. Available at
  15. Trifon Trifonov (2009): Dialectica Interpretation with Fine Computational Control. In: Klaus Ambos-Spies, Benedikt L\IeC öwe & Wolfgang Merkle: Mathematical Theory and Computational Practice, LNCS 5635. Springer Berlin/Heidelberg, pp. 467–477. Available at Proceedings of 5th Conference on Computability in Europe, CiE 2009, Heidelberg, Germany, July 19-24, 2009.
  16. Trifon Trifonov (2010): Quasi-linear Dialectica Extraction. In: Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo & Lu\'ıs Mendes Gomes: CiE, Lecture Notes in Computer Science 6158. Springer, pp. 417–426. Available at
  17. A. S. Troelstra (1973): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344. Springer-Verlag.

Comments and questions to:
For website issues: