{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:36:45Z","timestamp":1747888605601,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466773"},{"type":"electronic","value":"9783662466780"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_4","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"56-70","source":"Crossref","is-referenced-by-count":1,"title":["Game Semantics and Normalization by Evaluation"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Abel, A.: Normalization by Evaluation: Dependent Types and Impredicativity. Institut f\u00fcr Informatik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Habilitation thesis (May 2013)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-L\u00f6f type theory with one universe. In: 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIII. Electronic Notes in Theoretical Computer Science, pp. 17\u201340. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.02.025"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1006\/inco.2000.2930","volume":"163","author":"S. Abramsky","year":"2000","unstructured":"Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput.\u00a0163(2), 409\u2013470 (2000)","journal-title":"Inf. Comput."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Aehlig, K., Joachimski, F.: Operational aspects of untyped normalisation by evaluation. Mathematical Structures in Computer Science\u00a014(4) (2004)","DOI":"10.1017\/S096012950400427X"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Amadio, R., Curien, P.-L.: Domains and lambda-calculi, vol.\u00a046. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511983504"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed \u03bb-calculus. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pp. 203\u2013211 (July 1991)","DOI":"10.1109\/LICS.1991.151645"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic\u00a032, 209\u2013243 (1986)","journal-title":"Annals of Pure and Applied Logic"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science\u00a024(5) (2013)","DOI":"10.1017\/S0960129513000881"},{"key":"4_CR9","unstructured":"Clairambault, P., Murawski, A.S.: B\u00f6hm trees as higher-order recursive schemes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, Guwahati, India, December 12-14, pp. 91\u2013102 (2013)"},{"issue":"6","key":"4_CR10","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1017\/S0960129598002631","volume":"8","author":"P.-L. Curien","year":"1998","unstructured":"Curien, P.-L.: Abstract B\u00f6hm trees. Mathematical Structures in Computer Science\u00a08(6), 559\u2013591 (1998)","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR11","unstructured":"Curien, P.-L.: Notes on game semantics. From the authors web page (2006)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs","author":"P. Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 120\u2013134. Springer, Heidelberg (1996)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Program testing and the meaning explanations of intuitionistic type theory. In: Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\u00f6f, pp. 215\u2013241 (2012)","DOI":"10.1007\/978-94-007-4435-6_11"},{"issue":"2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.apal.2011.06.021","volume":"163","author":"P. Dybjer","year":"2012","unstructured":"Dybjer, P., Kuperberg, D.: Formal neighbourhoods, combinatory B\u00f6hm trees, and untyped normalization by evaluation. Ann. Pure Appl. Logic\u00a0163(2), 122\u2013131 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"4_CR15","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1051\/ita:2005026","volume":"39","author":"A. Filinski","year":"2005","unstructured":"Filinski, A., Rohde, H.K.: Denotational aspects of untyped normalization by evaluation. Theor. Inf. and App.\u00a039(3), 423\u2013453 (2005)","journal-title":"Theor. Inf. and App."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Harmer, R., Hyland, M., Melli\u00e8s, P.-A.: Categorical combinators for innocent strategies. In: 22nd IEEE Symposium on Logic in Computer Science, Wroclaw, Poland, Proceedings, pp. 379\u2013388. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.14"},{"issue":"2","key":"4_CR17","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"J.M.E. Hyland","year":"2000","unstructured":"Hyland, J.M.E., Luke Ong, C.-H.: On full abstraction for PCF: I, II, and III. Inf. Comput.\u00a0163(2), 285\u2013408 (2000)","journal-title":"Inf. Comput."},{"issue":"1-2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1999.2845","volume":"160","author":"G. McCusker","year":"2000","unstructured":"McCusker, G.: Games and full abstraction for FPC. Inf. Comput.\u00a0160(1-2), 1\u201361 (2000)","journal-title":"Inf. Comput."},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/0304-3975(94)90014-0","volume":"124","author":"A.M. Pitts","year":"1994","unstructured":"Pitts, A.M.: A co-induction principle for recursively defined domains. Theor. Comput. Sci.\u00a0124(2), 195\u2013219 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR20","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. Theor. Comput. Sci.\u00a05(3), 223\u2013255 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR21","unstructured":"Plotkin, G.D.: Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa Notes\u201d). Dept. of Computer Science, Univ. of Edinburgh (1981)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:41Z","timestamp":1747857461000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}