{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T05:59:52Z","timestamp":1780725592157,"version":"3.54.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,2,1]],"date-time":"2006-02-01T00:00:00Z","timestamp":1138752000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2006,2]]},"DOI":"10.1007\/s11225-006-6604-5","type":"journal-article","created":{"date-parts":[[2006,2,2]],"date-time":"2006-02-02T01:59:07Z","timestamp":1138845547000},"page":"25-49","source":"Crossref","is-referenced-by-count":21,"title":["Program Extraction from Normalization Proofs"],"prefix":"10.1007","volume":"82","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Berghofer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Letouzey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6604_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., \u2018Proving strong normalization of CC by modifying realizability semantics\u2019, in H. Barendregt and T. Nipkow, (eds.), Types for Proofs and Programs. International Workshop TYPES '93. Nijmegen, The Netherlands, May 1993, volume 806 of LNCS Springer Verlag, 1994, pp. 3\u201318.","DOI":"10.1007\/3-540-58085-9_70"},{"key":"6604_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., P. Dybjer, M. Hofmann, and P. Scott, \u2018Normalization by evaluation for typed lambda calculus with coproducts\u2019, in LICS '01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Washington, DC, USA, 2001, p. 303.","DOI":"10.1109\/LICS.2001.932506"},{"key":"6604_CR3","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., M. Hofmann, and T. Streicher, \u2018Reduction-free normalisation for a polymorphic system\u2019, in 11th Annual IEEE Symposium on Logic in Computer Science, 1996, pp. 98\u2013106.","DOI":"10.1109\/LICS.1996.561309"},{"key":"6604_CR4","doi-asserted-by":"crossref","unstructured":"Berger, U., \u2018Program extraction from normalization proofs\u2019, in M. Bezem, and J. F. Groote, (eds.), Typed Lambda Calculi and Applications, volume 664 of LNCS, Springer Verlag, 1993, pp. 91\u2013106.","DOI":"10.1007\/BFb0037100"},{"key":"6604_CR5","doi-asserted-by":"crossref","unstructured":"Berger, U., M. Eberl, and H. Schwichtenberg, \u2018Normalization by evaluation\u2019, in B. Moller, and J.V. Tucker, (eds.), Prospects for Hardware Foundations, volume 1546 of LNCS, Springer Verlag, 1998, pp. 117\u2013137.","DOI":"10.1007\/3-540-49254-2_4"},{"key":"6604_CR6","doi-asserted-by":"crossref","unstructured":"Berger, U., and H. Schwichtenberg, \u2018An inverse of the evaluation functional for typed A-calculus\u2019, in R. Vemuri, (ed.), Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos, 1991, pp. 203\u2013211.","DOI":"10.1109\/LICS.1991.151645"},{"key":"6604_CR7","unstructured":"Berghofer, S., Proofs, Programs and Executable Specifications in Higher Order Logic, PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen, 2003."},{"key":"6604_CR8","doi-asserted-by":"crossref","unstructured":"Biernacka, M., O. Danvy, and K. Stovring, \u2018Program extraction from proofs of weak head normalization\u2019, in Preliminary proceedings of MFPS XXI, Birmingham, UK, 2005, pp. 105\u2013123.","DOI":"10.7146\/brics.v12i12.21878"},{"key":"6604_CR9","doi-asserted-by":"crossref","unstructured":"Coquand, C., \u2018From semantics to rules: A machine assisted analysis\u2019, in E. Borger, Y. Gurevich, and K. Meinke, (eds.), Computer Science Logic, 7th Workshop, Swansea 1993, volume 832 of LNCS, Springer Verlag, 1994, pp. 91\u2013105.","DOI":"10.1007\/BFb0049326"},{"key":"6604_CR10","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1017\/S0960129596002150","volume":"7","author":"T. Coquand","year":"1997","unstructured":"Coquand, T., and P. Dybjer, \u2018Intuitionistic model constructions and normalization proofs\u2019, Mathematical Structures in Computer Science, 7: 73\u201394, 1997.","journal-title":"Mathematical Structures in Computer Science"},{"key":"6604_CR11","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. deBruijn","year":"1972","unstructured":"deBruijn, N. G., \u2018Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem\u2019, Indagationes Math., 34: 381\u2013392, 1972.","journal-title":"Indagationes Math."},{"key":"6604_CR12","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Kreisel, G., \u2018Interpretation of analysis by means of constructive functionals of finite types\u2019, in A. Heyting, (ed.), Constructivity in Mathematics, North-Holland, Amsterdam, 1959, pp. 101\u2013128."},{"key":"6604_CR13","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1016\/0890-5401(91)90068-D","volume":"91","author":"K. G. Larsen","year":"1991","unstructured":"Larsen, K. G., and G. Winskel, \u2018Using information systems to solve recursive domain equations\u2019, Information and Computation, 91: 232\u2013258, 1991.","journal-title":"Information and Computation"},{"key":"6604_CR14","doi-asserted-by":"crossref","unstructured":"Letouzey, P., \u2018A New Extraction for Coq\u2019, in H. Geuvers and F. Wiedijk, (eds.), Types for Proofs and Programs, Second International Workshop, TYPES 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003.","DOI":"10.1007\/3-540-39185-1_12"},{"key":"6604_CR15","unstructured":"Letouzey, P., Programmation fonctionnelle certifi\u00e9e - L'extraction de programmes dans I'assistant Coq. PhD thesis, Univ. Paris-Sud, 2004."},{"key":"6604_CR16","unstructured":"Letouzey, P., and B. Spitters, \u2018Implicit and noncomputational arguments using monads\u2019, 2005. Submitted for publication, available at http:\/\/www.lri.fr\/~letouzey\/download\/Letouzey_Spitters_05.pdf."},{"key":"6604_CR17","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C., \u2018Extracting F\u03c9's programs from proofs in the Calculus of Constructions\u2019, in Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM Press.","DOI":"10.1145\/75277.75285"},{"key":"6604_CR18","first-page":"1","volume":"11","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., and B. Werner, \u2018Synthesis of ML programs in the system Coq\u2019, J. Symbolic Computation, 11: 1\u201334, 1993.","journal-title":"J. Symbolic Computation"},{"key":"6604_CR19","unstructured":"Schwichtenberg, H., Minimal logic for computable functionals, 2004."},{"key":"6604_CR20","unstructured":"The Coq Development Team, The Coq Proof Assistant Reference Manual - Version 8.0, February 2004. Available at http:\/\/coq.inria.fr\/."},{"key":"6604_CR21","doi-asserted-by":"crossref","unstructured":"Troelstra, A. S., (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer Verlag, 1973.","DOI":"10.1007\/BFb0066739"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-006-6604-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-006-6604-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-006-6604-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T15:47:46Z","timestamp":1736264866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-006-6604-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,2]]}},"alternative-id":["6604"],"URL":"https:\/\/doi.org\/10.1007\/s11225-006-6604-5","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2]]}}}