{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:17Z","timestamp":1763467997608},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212980"},{"type":"electronic","value":"9783540247272"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24727-2_13","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:06:41Z","timestamp":1280761601000},"page":"167-181","source":"Crossref","is-referenced-by-count":6,"title":["A Denotational Account of Untyped Normalization by Evaluation"],"prefix":"10.1007","author":[{"given":"Andrzej","family":"Filinski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henning","family":"Korsholm Rohde","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Aehlig, K., Joachimski, F.: Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science (2004) (to appear), available from http:\/\/www.mathematik.uni-muenchen.de\/~aehlig\/pub\/03-nbe.ps","DOI":"10.1017\/S096012950400427X"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed \u03bb-calculus. In: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, The Netherlands, Amsterdam pp. 203\u2013211(July 1991)","DOI":"10.1109\/LICS.1991.151645"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1017\/S0960129596002150","volume":"7","author":"T. Coquand","year":"1997","unstructured":"Coquand, T., Dybjer, P.: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science\u00a07, 75\u201394 (1997)","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/10704567_23","volume-title":"Principles and Practice of Declarative Programming","author":"A. Filinski","year":"1999","unstructured":"Filinski, A.: A semantic account of type-directed partial evaluation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol.\u00a01702, pp. 378\u2013395. Springer, Heidelberg (1999)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Filinski, A., Rohde, H.K.: A denotational account of untyped normalization by evaluation (extended version). BRICS Report RS-03-40, University of Aarhus, Denmark (December 2003), Available from http:\/\/www.brics.dk\/RS\/03\/40\/","DOI":"10.7146\/brics.v10i40.21808"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-58027-1_3","volume-title":"Mathematical Foundations of Programming Semantics","author":"A.M. Pitts","year":"1994","unstructured":"Pitts, A.M.: Computational adequacy via \u2018mixed\u2019 inductive definitions. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol.\u00a0802, pp. 72\u201382. Springer, Heidelberg (1994)"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A.M. Pitts","year":"1996","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation\u00a0127(2), 66\u201390 (1996)","journal-title":"Information and Computation"},{"issue":"3","key":"13_CR8","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G.D. Plotkin","year":"1977","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science\u00a05(3), 223\u2013255 (1977)","journal-title":"Theoretical Computer Science"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/944705.944729","volume-title":"Eighth ACM SIGPLAN International Conference on Functional Programming","author":"M.R. Shinwell","year":"2003","unstructured":"Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programming with binders made simple. In: Eighth ACM SIGPLAN International Conference on Functional Programming, pp. 263\u2013274. ACM Press, Uppsala (2003)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24727-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T03:22:52Z","timestamp":1559359372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24727-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212980","9783540247272"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24727-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}