{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330107},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601784"},{"type":"electronic","value":"9783540447207"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60178-3_80","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:49:55Z","timestamp":1330260595000},"page":"77-97","source":"Crossref","is-referenced-by-count":15,"title":["Program extraction from classical proofs"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","unstructured":"Coquand, T.: A proof of Higman's lemma by structural induction. Manuscript (1993)"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0103100","volume":"699","author":"H. Friedman","year":"1978","unstructured":"Friedman, H.: Classically and intuitionistically provably recursive functions. In: Higher Set Theory, SLNCS 699 (1978) 21\u201328","journal-title":"Higher Set Theory, SLNCS"},{"key":"5_CR3","first-page":"236","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2 (1952) 236\u2013366","journal-title":"Proc. London Math. Soc."},{"key":"5_CR4","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Constructivity in Mathematics, North-Holland, (1959) 101\u2013128"},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"682","DOI":"10.2307\/2274322","volume":"50","author":"D. Leivant","year":"1985","unstructured":"Leivant, D.: Syntactic translations and provably recursive functions. Journal of Symbolic Logic 50 (1985), 682\u2013688","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR6","series-title":"Technical Report, Nr. 90-1151","volume-title":"PhD thesis","author":"C. Murthy","year":"1990","unstructured":"Murthy, C.: Extracting Constructive Content from Classical Proofs. PhD thesis. Technical Report, Nr. 90-1151, Dep. of Comp. Science, Cornell Univ, Ithaca, New York (1990)"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. Nash-Williams","year":"1963","unstructured":"Nash-Williams, C.: On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59 (1963) 833\u2013835","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF02007558","volume":"25","author":"K. Sch\u00fctte","year":"1985","unstructured":"Sch\u00fctte, K., Simpson, S.G: Ein in der reinen Zahlentheorie unbeweisbarer Satz \u00fcber endliche Folgen nat\u00fcrlicher Zahlen. Arch. Math. Logik 25 (1985) 75\u201389","journal-title":"Arch. Math. Logik"},{"key":"5_CR9","unstructured":"Schwichtenberg, H.: Proofs as programs. In: Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, Cambridge University Press (1992) 81\u2013113"},{"key":"5_CR10","unstructured":"Troelstra, A. S., van Dalen, D.: Constructivism in Mathematics Vol. 1. An Introduction. In: Studies in Logic and the Foundations of Mathematics, North-Holland 121 (1988)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Troelstra, A. S.: Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. SLNM 344 (1973)","DOI":"10.1007\/BFb0066739"}],"container-title":["Lecture Notes in Computer Science","Logic and Computational Complexity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60178-3_80.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:55:45Z","timestamp":1605628545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60178-3_80"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601784","9783540447207"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-60178-3_80","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}