{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T17:42:43Z","timestamp":1648662163442},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540419600","type":"print"},{"value":"9783540454137","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45413-6_15","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T08:51:43Z","timestamp":1186217503000},"page":"151-165","source":"Crossref","is-referenced-by-count":17,"title":["Normalization by Evaluation for the Computational Lambda-Calculus"],"prefix":"10.1007","author":[{"given":"Andrzej","family":"Filinski","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,4,25]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","volume-title":"6th International Conference","author":"T. Altenkirch","year":"1995","unstructured":"Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, 6th International Conference, number 953 in Lecture Notes in Computer Science, 1995."},{"key":"15_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications","author":"U. Berger","year":"1993","unstructured":"Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91\u2013106, Utrecht, The Netherlands, March 1993."},{"key":"15_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-49254-2_4","volume-title":"Prospects for Hardware Foundations (NADA)","author":"U. Berger","year":"1998","unstructured":"Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Prospects for Hardware Foundations (NADA), number 1546 in Lecture Notes in Computer Science, pages 117\u2013137, 1998."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed \u03bb-calculus. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203\u2013211, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151645"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"75","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:75\u201394, 1997.","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1017\/S0960129597002508","volume":"8","author":"D. \u010cubri\u010c","year":"1998","unstructured":"Djordje \u010cubri\u010c, Peter Dybjer, and Philip Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153\u2013192, 1998.","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","first-page":"367","volume-title":"Partial Evaluation \u2014 Practice and Theory; Proceedings of the 1998 DIKU Summer School","author":"O. Danvy","year":"1998","unstructured":"Olivier Danvy. Type-directed partial evaluation. In J. Hatcliff, T.\u00e6. Mogensen, and P. Thieman, editors, Partial Evaluation \u2014 Practice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367\u2013411. Springer-Verlag, Copenhagen, Denmark, July 1998."},{"key":"15_CR8","unstructured":"Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the APPSEM Workshop on Normalization by Evaluation. Department of Computer Science, University of Aarhus, May 1998. BRICS Note NS-98-1."},{"issue":"4","key":"15_CR9","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361\u2013391, December 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Andrzej Filinski. Representing layered monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 175\u2013188, San Antonio, Texas, January 1999.","DOI":"10.1145\/292540.292557"},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/10704567_23","volume-title":"International Conference on Principles and Practice of Declarative Programming","author":"A. Filinski","year":"1999","unstructured":"Andrzej Filinski. A semantic account of type-directed partial evaluation. In G. Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378\u2013395, Paris, France, September 1999."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 193\u2013202, Trento, Italy, July 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the SIGPLAN\u2019 93 Conference on Programming Language Design and Implementation, pages 237\u2013247, Albuquerque, New Mexico, June 1993.","DOI":"10.1145\/155090.155113"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 214\u2013224, Trento, Italy, July 1999.","DOI":"10.1109\/LICS.1999.782617"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Bernd Grobauer and Zhe Yang. The second Futamura projection for type-directed partial evaluation. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 22\u201332. ACM Press, January 2000.","DOI":"10.7146\/brics.v7i44.20211"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14\u201323, Pacific Grove, California, June 1989. IEEE.","DOI":"10.1109\/LICS.1989.39155"},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_20","volume-title":"Typed Lambda-Calculi and Applications","author":"A. Ohori","year":"1999","unstructured":"Atsushi Ohori. A Curry-Howard isomorphism for compilation and program execution. In J.-Y. Girard, editor, Typed Lambda-Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, L\u2019Aquila, Italy, April 1999."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Eijiro Sumii and Naoki Kobayashi. Online-and-offine partial evaluation: A mixed approach. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 12\u201321. ACM Press, January 2000.","DOI":"10.1145\/328691.328694"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45413-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:06:38Z","timestamp":1556737598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45413-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540419600","9783540454137"],"references-count":18,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-45413-6_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2001]]}}}