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