{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T16:02:40Z","timestamp":1787068960145,"version":"3.56.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540654612","type":"print"},{"value":"9783540492542","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49254-2_4","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T06:12:19Z","timestamp":1196489539000},"page":"117-137","source":"Crossref","is-referenced-by-count":27,"title":["Normalization by Evaluation"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Eberl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,6,11]]},"reference":[{"key":"4_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-60164-3_27","volume-title":"CTCS\u201995","author":"T. Altenkirch","year":"1995","unstructured":"Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In CTCS\u201995, Cambridge, volume 953 of Lecture Notes in Computer Science, pages 182\u2013199. Springer Verlag, Berlin, Heidelberg, New York, 1995."},{"key":"4_CR2","unstructured":"Holger Benl, Ulrich Berger, Helmut Schwichtenberg, Monika Seisenberger, and Wolfgang Zuber. Proof theory at work: Program development in the Minlog system. To appear: Automated Deduction-A Basis for Applications (eds) W. Bibel and P. Schmitt, Volume I: Foundations, Kluwer Academic Publishers, 1998."},{"key":"4_CR3","volume-title":"Habilitationsschrift","author":"U. Berger","year":"1997","unstructured":"Ulrich Berger. Continuous functionals of dependent and transfinite types. Habilitationsschrift, Mathematisches Institut der Universit\u00e4t M\u00fcnchen, 1997."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/LICS.1991.151645","volume-title":"Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science","author":"U. Berger","year":"1991","unstructured":"Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed \u03bb-calculus. In R. Vemuri, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203\u2013211. IEEE Computer Society Press, Los Alamitos, 1991."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1017\/S0960129596002150","volume":"7","author":"T. Coquand","year":"1997","unstructured":"Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:73\u201394, 1997.","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Roy L. Crole. Categories for Types. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9781139172707"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Djordje Cubric, Peter Dybjer, and Philip Scott. Normalization and the Yoneda embedding. To appear: Mathematical Structures in Computer Science, 1998.","DOI":"10.1017\/S0960129597002508"},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/3-540-61580-6_5","volume-title":"Partial Evaluation","author":"O. Danvy","year":"1996","unstructured":"Olivier Danvy. Pragmatics of type-directed partial evaluation. In O. Danvy, R. Gl\u00fcck, and P. Thiemann, editors, Partial Evaluation, volume 1110 of LNCS, pages 73\u201394. Springer Verlag, Berlin, Heidelberg, New York, 1996."},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Math., 34:381\u2013392, 1972.","journal-title":"Indagationes Math."},{"key":"4_CR10","unstructured":"J. Lambek and P. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986."},{"issue":"4","key":"4_CR11","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"John McCarthy. Recursive functions of symbolic expressions and their computation by machine. Communications of the ACM, 3(4):184\u2013195, 1960.","journal-title":"Communications of the ACM"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Helmut Schwichtenberg and Karl Stroetmann. From higher order terms to circuits. In M.L. Dalla Chiara, K. Doets, D. Mundici, and J. van Benthem, editors, Logic and Scientific Methods. Proceedings (Vol. 1) of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995, volume 259 of Synthese Library, pages 209\u2013220, Dordrecht, Boston, London, 1997. Kluwer Academic Publishers.","DOI":"10.1007\/978-94-017-0487-8_11"}],"container-title":["Lecture Notes in Computer Science","Prospects for Hardware Foundations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49254-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T08:11:48Z","timestamp":1557043908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49254-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654612","9783540492542"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-49254-2_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]}}}