References

1. Ulrich Berger (2005): Uniform Heyting Arithmetic.. Ann. Pure Appl. Logic 133(1–3), pp. 125–148. Available at http://dx.doi.org/10.1016/j.apal.2004.10.006.
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 http://doi.acm.org/10.1145/96709.96714.
7. Mircea-Dan Hernest (2007): Optimized programs from (non-constructive) proofs by the light (monotone) Dialectica interpretation. Ph.D. thesis. Ecole Polytechnique. Available at http://www.brics.dk/~danher/teza/thesfull.pdf.
8. Mircea-Dan Hernest & Trifon Trifonov (2010): Light Dialectica Revisited. Annals of Pure and Applied Logic 161(11), pp. 1313–1430. Available at http://dx.doi.org/10.1016/j.apal.2010.04.008.
9. Ulrich Kohlenbach (2008): Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer. Available at http://www.springer.com/mathematics/book/978-3-540-77532-4.
10. Yevgeniy Makarov (2006): Practical Program Extraction from Classical Proofs. Electr. Notes Theor. Comput. Sci. 155, pp. 521–542. Available at http://dx.doi.org/10.1016/j.entcs.2005.11.071.
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 http://dx.doi.org/10.1007/BFb0013061.
12. Diana Ratiu & Helmut Schwichtenberg (2009): Decorating Proofs. To appear in Mints Festschrift, draft at: http://www.math.lmu.de/ schwicht/papers/mints09/deco20090728.pdf.
13. Diana Ratiu & Trifon Trifonov (2009): Exploring the Computational Content of the Infinite Pigeonhole Principle. Draft at http://www.math.lmu.de/ trifonov/papers/iph.pdf. Available at http://dx.doi.org/10.1093/logcom/exq007. 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 http://dx.doi.org/10.1002/malq.200710045.
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 http://dx.doi.org/10.1007/978-3-642-03073-4_48. 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 http://dx.doi.org/10.1007/978-3-642-13962-8_46.
17. A. S. Troelstra (1973): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344. Springer-Verlag.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org