{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:47:04Z","timestamp":1764557224910},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642216909"},{"type":"electronic","value":"9783642216916"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21691-6_8","type":"book-chapter","created":{"date-parts":[[2011,6,11]],"date-time":"2011-06-11T05:31:26Z","timestamp":1307770286000},"page":"61-75","source":"Crossref","is-referenced-by-count":2,"title":["Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed \u03bb-Calculus"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Bourreau","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Salvati","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-58622-4_1","volume-title":"Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School","author":"S. Abramsky","year":"1999","unstructured":"Abramsky, S., McCusker, G.: Game semantics. In: Schwichtenberg, H., Berger, U. (eds.) Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pp. 1\u201356. Springer, Heidelberg (1999)"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1008254111992","volume":"8","author":"T. Aoto","year":"1999","unstructured":"Aoto, T.: Uniqueness of normal proofs in implicational intuitionistic logic. Journal of Logic, Language and Information\u00a08, 217\u2013242 (1999)","journal-title":"Journal of Logic, Language and Information"},{"key":"8_CR3","volume-title":"\u03bb-calculus: its syntax and semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: \u03bb-calculus: its syntax and semantics. Elsevier Science Publishers Ltd., Amsterdam (1984)"},{"issue":"3","key":"8_CR4","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1093\/logcom\/exi016","volume":"15","author":"S. Broda","year":"2005","unstructured":"Broda, S., Damas, L.: On long normal inhabitants of a type. J. Log. Comput.\u00a015(3), 353\u2013390 (2005)","journal-title":"J. Log. Comput."},{"key":"8_CR5","unstructured":"Belnap, N.: The two-property. Relevance Logic Newsletter, 173\u2013180 (1976)"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0168-0072(92)90073-9","volume":"56","author":"A. Blass","year":"1992","unstructured":"Blass, A.: A game semantics for linear logic. Annals of Pure and Applied Logic\u00a056, 183\u2013220 (1992)","journal-title":"Annals of Pure and Applied Logic"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"2263","DOI":"10.1007\/BF01629434","volume":"20","author":"A. Babaev","year":"1982","unstructured":"Babaev, A., Soloviev, S.: A coherence theorem for canonical morphism in cartesian closed categories. Journal of Soviet Mathematics\u00a020, 2263\u20132279 (1982)","journal-title":"Journal of Soviet Mathematics"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"de Groote, P.: Towards abstract categorial grammars. In: Proceedings of the Conference Association for Computational Linguistics, 39th Annual Meeting and 10th Conference of the European Chapter, pp. 148\u2013155 (2001)","DOI":"10.3115\/1073012.1073045"},{"key":"8_CR9","first-page":"207","volume-title":"POPL 1982: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"L. Damas","year":"1982","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL 1982: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 207\u2013212. ACM, New York (1982)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48959-2_10","volume-title":"Typed Lambda Calculi and Applications","author":"P. Gianantonio Di","year":"1999","unstructured":"Di Gianantonio, P., Franco, G., Honsell, F.: Game semantics for untyped \u03bb\u03b2 \u03b7-calculus. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 114\u2013128. Springer, Heidelberg (1999)"},{"key":"8_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511608865","volume-title":"Basic Simple Type Theory","author":"R.J. Hindley","year":"1997","unstructured":"Hindley, R.J.: Basic Simple Type Theory. Cambridge Press University, Cambridge (1997)"},{"key":"8_CR12","unstructured":"Hirokawa, S.: Balanced formulas, minimal formulas and their proofs. Technical report, Research Institute of Fundamental Information Science, Kyochu University (1991)"},{"key":"8_CR13","first-page":"285","volume-title":"Information and Computation","author":"J.M.E. Hyland","year":"2000","unstructured":"Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF. In: Information and Computation, vol.\u00a0163(2), ch. 2, pp. 285\u2013408. Elsevier Science B.V., Amsterdam (2000)"},{"key":"8_CR14","unstructured":"Huet, G.: R\u00e9solution d\u2019\u00e9quations dans les langages d\u2019ordre 1,2,.,\u03c9. PhD thesis, Universit\u00e9 Paris 7 (1976)"},{"key":"8_CR15","unstructured":"Hughes, D.J.D.: Hypergame Semantics: Full Completeness for System F. PhD thesis, Oxford University (2000)"},{"issue":"2","key":"8_CR16","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C.B. Jay","year":"1995","unstructured":"Jay, C.B., Ghani, N.: The virtues of \u03b7-expansion. J. of Functional Programming\u00a05(2), 135\u2013154 (1995); Also appeared as tech. report ECS-LFCS-92-243","journal-title":"J. of Functional Programming"},{"key":"8_CR17","unstructured":"Kanazawa, M.: Parsing and generation as Datalog queries. In: Proceedings of the 45th Annual Meeting of the Association for Computational Linguistics, Prague, pp. 176\u2013183. Association for Computational Linguistics (2007)"},{"issue":"1-2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/S0304-3975(00)00353-4","volume":"272","author":"A.D. Ker","year":"2002","unstructured":"Ker, A.D., Nickau, H., Ong, L.: Innocent game models of untyped \u03bb-calculus. Theoretical Computer Science\u00a0272(1-2), 247\u2013292 (2002)","journal-title":"Theoretical Computer Science"},{"key":"8_CR19","unstructured":"Lorenzen, P.: Ein dialogisches konstruktivitatskriterium. Infinitistic Methods, 193\u2013200 (1959)"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BF01973341","volume":"11","author":"K. Lorenz","year":"1968","unstructured":"Lorenz, K.: Dialogspiele als semantische grundlage von logikkalkiilen. Arch. Math. Logik Grundlag\u00a011, 32\u201355 (1968)","journal-title":"Arch. Math. Logik Grundlag"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF01404107","volume":"15","author":"G.E. Mints","year":"1977","unstructured":"Mints, G.E.: Closed categories and the theory of proofs. Journal of Mathematical Sciences\u00a015, 45\u201362 (1977)","journal-title":"Journal of Mathematical Sciences"},{"key":"8_CR22","unstructured":"Muskens, R.: Lambda Grammars and the Syntax-Semantics Interface. In: van Rooy, R., Stokhof, M. (eds.) Proceedings of the Thirteenth Amsterdam Colloquium, Amsterdam, pp. 150\u2013155 (2001)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-58140-5_25","volume-title":"Logical Foundations of Computer Science","author":"H. Nickau","year":"1994","unstructured":"Nickau, H.: Hereditarily sequential functionals. In: Nerode, A., Matiyasevich, Y. (eds.) LFCS 1994. LNCS, vol.\u00a0813, pp. 253\u2013264. Springer, Heidelberg (1994)"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10849-009-9110-0","volume":"19","author":"S. Salvati","year":"2010","unstructured":"Salvati, S.: On the membership problem for non-linear abstract categorial grammars. Journal of Logic, Language and Information\u00a019(2), 163\u2013183 (2010)","journal-title":"Journal of Logic, Language and Information"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21691-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,7]],"date-time":"2024-04-07T13:23:44Z","timestamp":1712496224000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21691-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642216909","9783642216916"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21691-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}