@unknown(uniformha,
 author       = "Ulrich Berger",
 year         = "2005",
 title        = "Uniform {H}eyting {A}rithmetic.",
 journal      = "Ann. Pure Appl. Logic",
 volume       = "133",
 number       = "1--3",
 pages        = "125--148",
 url          = "http://dx.doi.org/10.1016/j.apal.2004.10.006",
)
@unknown(bbs,
 author       = "Ulrich Berger and Wilfried Buchholz and Helmut Schwichtenberg",
 year         = "2002",
 title        = "Refined program extraction form classical proofs.",
 journal      = "Ann. Pure Appl. Logic",
 volume       = "114",
 number       = "1--3",
 pages        = "3--25",
)
@unknown(felleisen,
 author       = "Matthias Felleisen and Daniel P. Friedman",
 year         = "1989",
 title        = "A Syntactic Theory of Sequential State",
 journal      = "Theor. Comput. Sci.",
 volume       = "69",
 number       = "3",
 pages        = "243--287",
)
@unknown(friedman,
 author       = "Harvey Friedman",
 year         = "1978",
 title        = "Classically and intuitionistically provably recursive functions",
 journal      = "Lecture Notes in Mathematics",
 volume       = "669",
 pages        = "21--27",
)
@unknown(goedel,
 author       = "Kurt G{\"o}del",
 year         = "1958",
 title        = "{\"U}ber eine bisher noch nicht ben\"utzte {E}rweiterung des finiten {S}tandpunktes",
 journal      = "Dialectica",
 volume       = "12",
 pages        = "280--287",
)
@unknown(griffin,
 author       = "Timothy Griffin",
 year         = "1990",
 title        = "A Formulae-as-Types Notion of Control",
 booktitle    = "POPL",
 pages        = "47--58",
 url          = "http://doi.acm.org/10.1145/96709.96714",
)
@unknown(danhernest,
 author       = "Mircea-Dan Hernest",
 year         = "2007",
 title        = "Optimized programs from (non-constructive) proofs by the light (monotone) Dialectica interpretation",
 type         = "Ph.D. thesis",
 school       = "Ecole Polytechnique",
 url          = "http://www.brics.dk/~danher/teza/thesfull.pdf",
)
@unknown(ldrev,
 author       = "Mircea-Dan Hernest and Trifon Trifonov",
 year         = "2010",
 title        = "Light Dialectica Revisited",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "161",
 number       = "11",
 pages        = "1313--1430",
 url          = "http://dx.doi.org/10.1016/j.apal.2010.04.008",
)
@unknown(kohlenbook,
 author       = "Ulrich Kohlenbach",
 year         = "2008",
 title        = "Applied Proof Theory: Proof Interpretations and their Use in Mathematics",
 series       = "Springer Monographs in Mathematics",
 publisher    = "Springer",
 url          = "http://www.springer.com/mathematics/book/978-3-540-77532-4",
)
@unknown(makaroventcs,
 author       = "Yevgeniy Makarov",
 year         = "2006",
 title        = "Practical Program Extraction from Classical Proofs",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "155",
 pages        = "521--542",
 url          = "http://dx.doi.org/10.1016/j.entcs.2005.11.071",
)
@unknown(parigot,
 author       = "Michel Parigot",
 year         = "1992",
 title        = "$\lambda \mu $-Calculus: An Algorithmic Interpretation of Classical Natural Deduction",
 editor       = "Andrei Voronkov",
 booktitle    = "LPAR",
 series       = "Lecture Notes in Computer Science",
 volume       = "624",
 publisher    = "Springer",
 pages        = "190--201",
 url          = "http://dx.doi.org/10.1007/BFb0013061",
)
@unknown(decorating,
 author       = "Diana Ratiu and Helmut Schwichtenberg",
 year         = "2009",
 title        = "Decorating Proofs",
 howpublished = "To appear in Mints Festschrift, draft at: \url {http://www.math.lmu.de/ schwicht/papers/mints09/deco20090728.pdf}",
)
@unknown(iph,
 author       = "Diana Ratiu and Trifon Trifonov",
 year         = "2009",
 title        = "Exploring the Computational Content of the Infinite Pigeonhole Principle",
 howpublished = "Draft at \url {http://www.math.lmu.de/ trifonov/papers/iph.pdf}",
 url          = "http://dx.doi.org/10.1093/logcom/exq007",
 note         = "To appear in Proceedings of CiE 2008, Journal of Logic and Computation",
)
@unknown(schwichtwfi,
 author       = "Helmut Schwichtenberg",
 year         = "2008",
 title        = "Dialectica interpretation of well-founded induction",
 journal      = "Mathematical Logic Quarterly",
 volume       = "54",
 number       = "3",
 pages        = "229--239",
 url          = "http://dx.doi.org/10.1002/malq.200710045",
)
@unknown(dialfine,
 author       = "Trifon Trifonov",
 year         = "2009",
 title        = "Dialectica Interpretation with Fine Computational Control",
 editor       = "Klaus Ambos-Spies and Benedikt L\IeC {\"o}we and Wolfgang Merkle",
 booktitle    = "Mathematical Theory and Computational Practice",
 series       = "LNCS",
 volume       = "5635",
 publisher    = "Springer Berlin/Heidelberg",
 pages        = "467--477",
 url          = "http://dx.doi.org/10.1007/978-3-642-03073-4_48",
 note         = "Proceedings of 5th Conference on Computability in Europe, CiE 2009, Heidelberg, Germany, July 19-24, 2009",
)
@unknown(quasilin,
 author       = "Trifon Trifonov",
 year         = "2010",
 title        = "Quasi-linear Dialectica Extraction",
 editor       = "Fernando Ferreira and Benedikt L{\"o}we and Elvira Mayordomo and Lu\'{\i }s Mendes Gomes",
 booktitle    = "CiE",
 series       = "Lecture Notes in Computer Science",
 volume       = "6158",
 publisher    = "Springer",
 pages        = "417--426",
 url          = "http://dx.doi.org/10.1007/978-3-642-13962-8_46",
)
@unknown(troelstra,
 author       = "A. S. Troelstra",
 year         = "1973",
 title        = "Metamathematical Investigation of Intuitionistic Arithmetic and Analysis",
 series       = "Lecture Notes in Mathematics",
 volume       = "344",
 publisher    = "Springer-Verlag",
)