{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T19:40:04Z","timestamp":1748461204366,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662476659"},{"type":"electronic","value":"9783662476666"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-47666-6_3","type":"book-chapter","created":{"date-parts":[[2015,6,19]],"date-time":"2015-06-19T07:46:47Z","timestamp":1434700007000},"page":"31-43","source":"Crossref","is-referenced-by-count":3,"title":["Games for Dependent Types"],"prefix":"10.1007","author":[{"given":"Samson","family":"Abramsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radha","family":"Jagadeesan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthijs","family":"V\u00e1k\u00e1r","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,20]]},"reference":[{"key":"3_CR1","unstructured":"Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter. Manuscript, 235 (2005). http:\/\/www.cs.nott.ac.uk\/txa\/publ\/ydtm.pdf"},{"issue":"01","key":"3_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S Awodey","year":"2009","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146(01), 45\u201355 (2009)","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"3_CR3","unstructured":"HoTTbaki, U.: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). http:\/\/homotopytypetheory.org\/book"},{"issue":"02","key":"3_CR4","doi-asserted-by":"publisher","first-page":"543","DOI":"10.2307\/2275407","volume":"59","author":"S Abramsky","year":"1994","unstructured":"Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. The Journal of Symbolic Logic 59(02), 543\u2013574 (1994)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"3_CR5","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"JME Hyland","year":"2000","unstructured":"Hyland, J.M.E., Ong, C.H.: On full abstraction for PCF: I, II, and III. Information and Computation 163(2), 285\u2013408 (2000)","journal-title":"Information and Computation"},{"issue":"2","key":"3_CR6","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. Information and Computation 163(2), 409\u2013470 (2000)","journal-title":"Information and Computation"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.apal.2004.10.002","volume":"133","author":"S Abramsky","year":"2005","unstructured":"Abramsky, S., Jagadeesan, R.: A game semantics for generic polymorphism. Annals of Pure and Applied Logic 133(1), 3\u201337 (2005)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Laird, J.: Full abstraction for functional languages with control. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS 1997, pp. 58\u201367. IEEE (1997)","DOI":"10.1109\/LICS.1997.614931"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, pp. 334\u2013344. IEEE (1998)","DOI":"10.1109\/LICS.1998.705669"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.H., Stark, I.D.: Nominal games and full abstraction for the nu-calculus. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 150\u2013159. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319609"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0028004","volume-title":"Computer Science Logic","author":"S Abramsky","year":"1998","unstructured":"Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M., Thomas, W. (eds.) Computer Science Logic. Lecture Notes in Computer Science, vol. 1414, pp. 1\u201317. Springer, Berlin Heidelberg (1998)"},{"key":"3_CR12","unstructured":"Streicher, T.: Investigations into intensional type theory (1993). http:\/\/www.mathematik.tu-darmstadt.de\/streicher\/HabilStreicher.pdf"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Extensional Constructs in Intensional Type Theory, pp. 13\u201354. Springer (1997)","DOI":"10.1007\/978-1-4471-0963-1_2"},{"key":"3_CR14","unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: 19th International Conference on Types for Proofs and Programs, TYPES 2013, vol. 26, pp. 107\u2013128 (2014)"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0168-0072(90)90044-3","volume":"48","author":"E Palmgren","year":"1990","unstructured":"Palmgren, E., Stoltenberg-Hansen, V.: Domain interpretations of Martin-L\u00f6f\u2019s partial type theory. Annals of Pure and Applied Logic 48(2), 135\u2013196 (1990)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.entcs.2009.07.088","volume":"249","author":"S Abramsky","year":"2009","unstructured":"Abramsky, S., Jagadeesan, R.: Game semantics for access control. Electronic Notes in Theoretical Computer Science 249, 135\u2013156 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-662-46678-0_7","volume-title":"Foundations of Software Science and Computation Structures","author":"M V\u00e1k\u00e1r","year":"2015","unstructured":"V\u00e1k\u00e1r, M.: A categorical semantics for linear logical frameworks. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 102\u2013116. Springer, Heidelberg (2015)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D., Maibaum, T., (eds.) Handbook of Logic in Computer Science, vol. 5, pp. 39\u2013128. OUP (2000)","DOI":"10.1093\/oso\/9780198537816.003.0005"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Axioms for definability and full completeness. In: Proof, Language and Interaction: Essays in Honour of Robin, pp. 55\u201375. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0007"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-47666-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T19:03:50Z","timestamp":1748459030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-47666-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662476659","9783662476666"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-47666-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}