{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:05:10Z","timestamp":1773097510803,"version":"3.50.1"},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037118","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"361-375","source":"Crossref","is-referenced-by-count":76,"title":["A logic for parametric polymorphism"],"prefix":"10.1007","author":[{"given":"Gordon","family":"Plotkin","sequence":"first","affiliation":[]},{"given":"Mart\u00edn","family":"Abadi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Martin Abadi, Luca Cardelli and Pierre-Louis Curien. Formal parametric polymorphism. To Appear in proceedings of Principles of Prgramming Languages '93."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science, 389","first-page":"357","volume-title":"Category Theory and Computer Science","author":"A. Peter","year":"1989","unstructured":"Peter Aczel and Nax Mendler. A final co-algebra theorem. In D. H. Pitt et al., editors, Category Theory and Computer Science Lecture Notes in Computer Science, 389:357\u2013365 Berlin, 1989. Springer-Verlag."},{"issue":"1","key":"25_CR3","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E. S. Bainbridge","year":"1990","unstructured":"E. S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35\u201364, January 15 1990. Corrigendum in (3) 71, 10 April 1990, p. 431.","journal-title":"Theoretical Computer Science"},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"Corrado B\u00f6hm and A. Berarducci. Automatic synthesis of typed \u039b-programs on term algebras. Theoretical Computer Science, 39:85\u2013114, 1985.","journal-title":"Theoretical Computer Science"},{"key":"25_CR5","series-title":"volume 526 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"750","DOI":"10.1007\/3-540-54415-1_73","volume-title":"Theoretical Aspects of Computer Software","author":"L. Cardelli","year":"1991","unstructured":"Luca Cardelli, Simone Martini, John Mitchell, and Andre Scedrov. An extension of system F with subtyping. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 750\u2013770, Berlin, 1991. Springer-Verlag."},{"key":"25_CR6","series-title":"volume 526 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"731","DOI":"10.1007\/3-540-54415-1_72","volume-title":"Theoretical Aspects of Computer Software","author":"P. Curien","year":"1991","unstructured":"Pierre-Louis Curien and Giorgio Ghelli. Subtyping+extensionality: Confluence of \u03b2\u03b7top reduction in F\u2264. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 731\u2013749, Berlin, 1991. Springer-Verlag."},{"issue":"1","key":"25_CR7","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1017\/S0960129500001134","volume":"2","author":"P. Curien","year":"1992","unstructured":"Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in F\u2264. Mathematical Structures in Computer Science, 2(1):55\u201392, March 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"25_CR8","unstructured":"Ryu Hasegawa. Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science, 1990. To appear."},{"key":"25_CR9","series-title":"volume 526 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-54415-1_61","volume-title":"Theoretical Aspects of Computer Software","author":"R. Hasegawa","year":"1991","unstructured":"Ryu Hasegawa. Parametricity of extensionally collapsed models of polymorphism and their categorical properties. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 495\u2013512, Berlin, 1991. Springer-Verlag."},{"key":"25_CR10","volume-title":"Lecture Notes in Computer Science","author":"Q. Ma","year":"1992","unstructured":"QingMing Ma and John C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, editors, Proceedings of the 1991 Mathematical Foundations of Programming Semantics Conference, Lecture Notes in Computer Science, Berlin, 1992. Springer-Verlag. To appear."},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Harry Mairson. Outline of a proof theory of parametricity. In Proc. 5th International Symp. on Functional Programming Languages and Computer Architecture, Springer-Verlag, 1991.","DOI":"10.1007\/3540543961_15"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 37\u201351, 1985.","DOI":"10.1145\/318593.318606"},{"key":"25_CR13","first-page":"195","volume-title":"Logical Foundations of Functional Programming","author":"J. C. Mitchell","year":"1990","unstructured":"John C. Mitchell. A type inference approach to reduction properties and semantics of polymorphic expressions (summary). In G. Huet, editor, Logical Foundations of Functional Programming, pages 195\u2013212, Reading, 1990. Addison-Wesley."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"John C. Mitchell. On the equivalence of data representations. In V. Lifshitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, pages 305\u2013330, 1991.","DOI":"10.1016\/B978-0-12-450010-5.50023-2"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science, 283","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-18508-9_18","volume-title":"Category Theory and Computer Science","author":"A. M. Pitts","year":"1987","unstructured":"Andrew M. Pitts. Polymorphism is set-theoretic, constructively. In D. H. Pitt et al., editors, Category Theory and Computer Science Lecture Notes in Computer Science, 283:12\u201339 Berlin, 1987. Springer-Verlag."},{"key":"25_CR16","unstructured":"Andrew M. Pitts. A co-induction principle for recursively defined domains. To appear in Theoretical Computer Science."},{"key":"25_CR17","first-page":"513","volume-title":"Information Processing 83","author":"J. C. Reynolds","year":"1983","unstructured":"John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513\u2013523, Amsterdam, 1983. Elsevier Science Publishers B. V. (North-Holland)."},{"key":"25_CR18","first-page":"127","volume-title":"Logical Foundations of Functional Programming","author":"J. C. Reynolds","year":"1990","unstructured":"John C. Reynolds and Gordon D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. In G. Huet, editor, Logical Foundations of Functional Programming, pages 127\u2013152, Reading, 1990. Addison-Wesley."},{"key":"25_CR19","series-title":"London Mathematical Society Lecture Note Series, 177","first-page":"270","volume-title":"Applications of Categories in Computer Science","author":"M. B. Smyth","year":"1991","unstructured":"Michael B. Smyth. I-categories and duality. In M. P. Fourman, P. T. Johnstone and A. M. Pitts, Applications of Categories in Computer Science London Mathematical Society Lecture Note Series, 177:270\u2013287, Cambridge, 1991 Cambridge University Press."},{"key":"25_CR20","volume-title":"Lecture Notes","author":"C. Strachey","year":"1967","unstructured":"Christopher Strachey. Fundamental concepts in programming languages. Lecture Notes, International Summer School in Programming Languages, Copenhagen, Unpublished, August 1967."},{"key":"25_CR21","unstructured":"Philip Wadler. Recursive types in polymorphic second-order lambda-calculus Draft, University of Glasgow 1990."},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science, 39","first-page":"118","volume-title":"Category Theory and Computer Science","author":"G. C. Wraith","year":"1989","unstructured":"Gavin C. Wraith. A note on categorical datatypes. In A. M. Pitts and A. Poign\u00e9, editors, Category Theory and Computer Science Lecture Notes in Computer Science, 39:118\u2013127, Berlin, 1989, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037118.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:08Z","timestamp":1607552528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037118"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0037118","relation":{},"subject":[]}}