{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:04Z","timestamp":1761596944130},"publisher-location":"Berlin\/Heidelberg","reference-count":9,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037100","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"91-106","source":"Crossref","is-referenced-by-count":29,"title":["Program extraction from normalization proofs"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"U. Berger, H. Schwichtenberg, An Inverse of the Evaluation Functional for Typed \u03bb-calculus, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, (1991) 203\u2013211.","DOI":"10.1109\/LICS.1991.151645"},{"key":"7_CR2","unstructured":"C. Coquand, A proof of normalization for simply typed lambda calculus written in ALF, Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden (1992) 80\u201387."},{"key":"7_CR3","volume-title":"PX: a system extracting programs from proofs","author":"S. Hayashi","year":"1987","unstructured":"S. Hayashi, PX: a system extracting programs from proofs, Kyoto University, Japan (1987)."},{"key":"7_CR4","unstructured":"V. Gaspes, J. S. Smith, Machine Checked Normalization Proofs for Typed Combinator Calculi, Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden (1992) 168\u2013192."},{"key":"7_CR5","unstructured":"G. Kreisel, Interpretation of analysis by means of functionals of finite type, in Constructivity in Mathematics (1959) 101\u2013128."},{"key":"7_CR6","unstructured":"C. Paulin-Mohring, B. Werner, Synthesis of ML programs in the system Coq, Submitted to the Journal of Symbolic Computations (1992)."},{"key":"7_CR7","unstructured":"H. Schwichtenberg, Proofs as Programs, Leeds: Proof Theory '90 (P. Aczel, H. Simmons, Editors 1990)."},{"issue":"2","key":"7_CR8","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait, Intensional Interpretation of Functionals of Finite Type I, Journal of Symbolic Logic 32(2) (1967) 198\u2013212.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, SLNM 344 (1973).","DOI":"10.1007\/BFb0066739"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037100.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:01Z","timestamp":1607552521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037100"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/bfb0037100","relation":{},"subject":[]}}