{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T20:25:25Z","timestamp":1794515125946,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496299","type":"print"},{"value":"9783662496305","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_1","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T05:04:32Z","timestamp":1458536672000},"page":"3-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Comprehensive Parametric Polymorphism: Categorical Models and Type Theory"],"prefix":"10.1007","author":[{"given":"Neil","family":"Ghani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fredrik","family":"Nordvall Forsberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alex","family":"Simpson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1&2","key":"1_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","volume":"121","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. Theor. Comput. Sci. 121(1&2), 9\u201358 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Atkey, R., Ghani, N., Johann, P.: A relationally parametric model of dependent type theory. In: Jagannathan, S., Sewell, P. (eds.), POPL, pp. 503\u2013515. ACM (2014)","DOI":"10.1145\/2535838.2535852"},{"issue":"2","key":"1_CR3","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125\u2013154 (1991)","journal-title":"J. Funct. Program."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bernardy, J.-P., Coquand, T., Moulin, G.: A presheaf model of parametric type theory. In: Ghica, D.R. (ed.), MFPS, ENTCS, pp. 17\u201333. Elsevier (2015)","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","volume":"22","author":"J-P Bernardy","year":"2012","unstructured":"Bernardy, J.-P., Jansson, P., Paterson, R.: Proofs for free. J. Funct. Program. 22, 107\u2013152 (2012)","journal-title":"J. Funct. Program."},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S0960129505004834","volume":"15","author":"E M\u00f8gelberg","year":"2005","unstructured":"M\u00f8gelberg, E.: Categorical models for Abadi and Plotkin\u2019s logic for parametricity. Math. Struct. Comput. Sci. 15, 709\u2013772 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"key":"1_CR7","unstructured":"Dunphy, B.: Parametricity as a notion of uniformity in reflexive graphs. Ph.D. thesis, University of Illinois (2002)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Dunphy, B., Reddy, U.: Parametric limits. In: LICS, pp. 242\u2013251 (2004)","DOI":"10.1109\/LICS.2004.1319618"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Ghani, N., Johann, P., Nordvall Forsberg, F., Orsanigo, F., Revell, T.: Bifibrational functorial semantics of parametric polymorphism. In: Ghica, D.R. (ed.) MFPS, ENTCS, pp. 67\u201383. Elsevier (2015)","DOI":"10.1016\/j.entcs.2015.12.011"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-662-47709-0_7","volume-title":"Logic, Language, Information, and Computation","author":"N Ghani","year":"2015","unstructured":"Ghani, N., Nordvall Forsberg, F., Orsanigo, F.: Parametric polymorphism \u2014 universally. In: de Paiva, V., de Queiroz, R., Moss, L.S., Leivant, D., de Oliveira, A. (eds.) WoLLIC 2015. LNCS, vol. 9160, pp. 81\u201392. Springer, Heidelberg (2015)"},{"key":"1_CR11","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, University of Paris VII (1972)"},{"key":"1_CR12","unstructured":"Hermida, C.: Fibrational relational polymorphism (2006). http:\/\/maggie.cs.queensu.ca\/chermida\/papers\/FibRelPoly.pdf"},{"key":"1_CR13","first-page":"149","volume":"303","author":"C Hermida","year":"2014","unstructured":"Hermida, C., Reddy, U., Robinson, E.: Logical relations and parametricity \u2013 a Reynolds programme for category theory and programming languages. ENTCS 303, 149\u2013180 (2014)","journal-title":"ENTCS"},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B Jacobs","year":"1993","unstructured":"Jacobs, B.: Comprehension categories and the semantics of type dependency. Theor. Comput. Sci. 107(2), 169\u2013207 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR15","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0014552","volume-title":"Theoretical Aspects of Computer Software","author":"Y Kinoshita","year":"1997","unstructured":"Kinoshita, Y., O\u2019Hearn, P.W., Power, J., Takeyama, M., Tennent, R.D.: An axiomatic approach to binary logical relations with applications to data refinement. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. LNCS, vol. 1281, pp. 191\u2013212. Springer, Heidelberg (1997)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Dreyer, D.: Internalizing relational parametricity in the extensional calculus of constructions. In: Ronchi, S., Rocca, D. (eds.) CSL, pp. 432\u2013451 (2013)","DOI":"10.4324\/9780203881347-22"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1090\/pspum\/017\/0257175","volume":"17","author":"FW Lawvere","year":"1970","unstructured":"Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. Appl. Categorical Algebra 17, 1\u201314 (1970)","journal-title":"Appl. Categorical Algebra"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-55511-0_1","volume-title":"Mathematical Foundations of Programming Semantics","author":"Q Ma","year":"1991","unstructured":"Ma, Q., Reynolds, J.C.: Types, abstraction, and parametric polymorphism, part 2. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Mathematical Foundations of Programming Semantics. LNCS, vol. 598, pp. 1\u201340. Springer, Heidelberg (1991)"},{"issue":"3","key":"1_CR20","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/210346.210425","volume":"42","author":"PW O\u2019Hearn","year":"1995","unstructured":"O\u2019Hearn, P.W., Tennent, R.D.: Parametricity and local variables. J. ACM 42(3), 658\u2013709 (1995)","journal-title":"J. ACM"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G Plotkin","year":"1993","unstructured":"Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) Typed Lambda Calculi and Applications. LNCS, vol. 664, pp. 361\u2013375. Springer, Heidelberg (1993)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Programming Symposium","author":"J Reynolds","year":"1974","unstructured":"Reynolds, J.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408\u2013425. Springer, Heidelberg (1974)"},{"key":"1_CR23","unstructured":"Reynolds, J.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.), Information Processing, pp. 513\u2013523 (1983)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Robinson, E.P., Rosolini, G.: Reflexive graphs and parametric polymorphism. In: LICS, pp. 364\u2013371. IEEE Computer Society (1994)","DOI":"10.1109\/LICS.1994.316053"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"969","DOI":"10.2307\/2273831","volume":"52","author":"RAG Seely","year":"1987","unstructured":"Seely, R.A.G.: Categorical semantics for higher order polymorphic lambda calculus. J. Symbolic Logic 52, 969\u2013989 (1987)","journal-title":"J. Symbolic Logic"},{"issue":"1\u20132","key":"1_CR26","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1023\/A:1010000313106","volume":"13","author":"C Strachey","year":"2000","unstructured":"Strachey, C.: Fundamental concepts in programming languages. High. Order Symbolic Comput. 13(1\u20132), 11\u201349 (2000)","journal-title":"High. Order Symbolic Comput."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Stoy, J.E. (ed.) FPCA, pp. 347\u2013359. ACM (1989)","DOI":"10.1145\/99370.99404"}],"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-49630-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T17:29:58Z","timestamp":1748798998000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_1","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}