J. Avigad & S. Feferman (1998):
Gödel's functional (``Dialectica") interpretation.
In: S. R. Buss: Handbook of proof theory,
Studies in Logic and the Foundations of Mathematics 137.
North Holland, Amsterdam,
pp. 337–405,
doi:10.1016/S0049-237X(98)80020-7.
U. Berger (2004):
A Computational Interpretation of Open Induction.
In: F. Titsworth: Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science.
IEEE Computer Society,
pp. 326–334,
doi:10.1109/LICS.2004.1319627.
U. Berger & M. Seisenberger (2005):
Applications of inductive definitions and choice principles to program synthesis.
In: From Sets and Types to Topology and Analysis Towards Practicable Foundations for Constructive Mathematics,
Oxford Logic Guides 48.
OUP,
pp. 137–148,
doi:10.1093/acprof:oso/9780198566519.003.0008.
E. Cichon & E. Bittar (1998):
Ordinal Recursive Bounds for Higman's Theorem.
Theoretical Computer Science 201,
pp. 63–84,
doi:10.1016/S0304-3975(97)00009-1.
T. Coquand (1991):
Constructive Topology and Combinatorics.
In: Constructivity in Computer Science,
LNCS 613,
pp. 159–164.
T. Coquand & D. Fridlender (1993):
A proof of Higman's lemma by structural induction.
Unpublished Manuscript,
doi:10.1007/BFb0021089.
M. H. Escardó & P. Oliva (2010):
Selection Functions, Bar Recursion, and Backward Induction.
Mathematical Structures in Computer Science 20(2),
pp. 127–168,
doi:10.1017/S0960129509990351.
M. H. Escardó & P. Oliva (2011):
Sequential games and optimal strategies.
Royal Society Proceedings A 467,
pp. 1519–1545,
doi:10.1098/rspa.2010.0471.
G. Higman (1952):
Ordering by Divisibility in Abstract Algebras.
Proc. London Math. Soc. 2,
pp. 326–336,
doi:10.1112/plms/s3-2.1.326.
U. Kohlenbach (2008):
Applied Proof Theory: Proof Interpretations and their Use in Mathematics.
Monographs in Mathematics.
Springer.
J.B. Kruskal (1960):
Well-quasi-ordering, the tree theorem, and Vázsonyi's conjecture.
Trans. American Math. Soc. 95,
pp. 210–225,
doi:10.1090/S0002-9947-1960-0111704-1.
C. Murthy (1990):
Extracting Constructive Content from Classical Proofs.
Cornell University.
C. St. J. A. Nash-William (1963):
On Well-Quasi-Ordering Finite Trees.
Proc. Cambridge Phil. Soc. 59,
pp. 833–835,
doi:10.1017/S0305004100003844.
P. Oliva (2006):
Understanding and using Spector's bar recursive interpretation of classical analysis.
In: A. Beckmann, U. Berger, B. Löwe & J. V. Tucker: Proceedings of CiE'2006, LNCS 3988.
Springer,
pp. 423–234,
doi:10.1007/11780342_44.
P. Oliva & T. Powell (2011):
A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions.
To appear: Math. Struct. in Comp. Science. Preprint available at http://arxiv.org/abs/1204.5631.
P. Oliva & T. Powell (2012):
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis.
Preprint available at http://arxiv.org/abs/1204.5244.
M. Seisenberger (2003):
On the Constructive Content of Proofs.
Ludwigs-Maximilians-Universität München.
C. Spector (1962):
Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics.
In: F. D. E. Dekker: Recursive Function Theory: Proc. Symposia in Pure Mathematics 5.
American Mathematical Society, Providence, Rhode Island,
pp. 1–27.
W. Veldman (2004):
An Intuitionistic Proof of Kruskal's Theorem.
Archive for Mathematical Logic 43(2),
pp. 215–264,
doi:10.1007/s00153-003-0207-x.
eptcs@eptcs.org