{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:10:21Z","timestamp":1773097821275,"version":"3.50.1"},"reference-count":64,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":8598,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1990,1]]},"DOI":"10.1016\/0304-3975(90)90151-7","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:07:16Z","timestamp":1027652836000},"page":"35-64","source":"Crossref","is-referenced-by-count":107,"title":["Functorial polymorphism"],"prefix":"10.1016","volume":"70","author":[{"given":"E.S.","family":"Bainbridge","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.J.","family":"Freyd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.J.","family":"Scott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(90)90151-7_BIB1","series-title":"Logical Foundations of Functional Programming, Proceedings","article-title":"Functorial polymorphism","author":"Bainbridge","year":"1987"},{"key":"10.1016\/0304-3975(90)90151-7_BIB2","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","DOI":"10.1016\/S0049-237X(08)71818-4","article-title":"The Lambda Calculus","author":"Barendregt","year":"1984"},{"key":"10.1016\/0304-3975(90)90151-7_BIB3","series-title":"Programming in Ada","author":"Barnes","year":"1981"},{"key":"10.1016\/0304-3975(90)90151-7_BIB4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","article-title":"Automatic synthesis of typed A-programs on term algebras","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90151-7_BIB5_1","article-title":"Extensional models for polymorphism","volume":"250","author":"Breazu-Tennen","year":"1987"},{"issue":"1, 2","key":"10.1016\/0304-3975(90)90151-7_BIB5_2","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(88)90097-7","article-title":"Extensional models for polymorphism","volume":"59","author":"Breazu-Tannen","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90151-7_BIB6","series-title":"Proc. 3rd IEEE Symp. on Logic in Computer Science","first-page":"38","article-title":"A modest model of records, inheritance, and bounded quantification","author":"Bruce","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB7","doi-asserted-by":"crossref","unstructured":"K.B. Bruce, A.R. Meyer and J.C. Mitchell, The semantics of second-order lambda calculus, Inform. and Comput. to appear.","DOI":"10.1016\/0890-5401(90)90044-I"},{"key":"10.1016\/0304-3975(90)90151-7_BIB8","first-page":"23","article-title":"A categorical approach to realizability and polymorphic types","volume":"298","author":"Carboni","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB9","author":"Cardelli","year":"1988","journal-title":"Time for a new language"},{"key":"10.1016\/0304-3975(90)90151-7_BIB10","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","article-title":"On understanding types, data abstraction, and polymorphism","volume":"17","author":"Cardelli","year":"1985","journal-title":"Comput. Surveys"},{"key":"10.1016\/0304-3975(90)90151-7_BIB11","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/0304-3975(90)90151-7_BIB12","series-title":"Proc: EUROCAL '85","first-page":"151","article-title":"Constructions: a higher-order proof system for mechanizing mathematics","volume":"203","author":"Coquand","year":"1985"},{"key":"10.1016\/0304-3975(90)90151-7_BIB13","first-page":"344","article-title":"Di-domains as a model of polymorphism","volume":"298","author":"Coquand","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB14","doi-asserted-by":"crossref","unstructured":"T. Coquand, C.A. Gunter and G. Winskel, Domain theoretical models for polymorphism, Inform. and Comput. to appear.","DOI":"10.1016\/0890-5401(89)90068-0"},{"key":"10.1016\/0304-3975(90)90151-7_BIB15","author":"Cousineau","year":"1987","journal-title":"CAML, Lectures at the University of Texas Programming Institute on the Logical Foundations of Functional Programming"},{"key":"10.1016\/0304-3975(90)90151-7_BIB16","series-title":"Reports of the Midwest Category Seminar IV","first-page":"126","article-title":"Dinatural transformations","volume":"137","author":"Dubuc","year":"1970"},{"key":"10.1016\/0304-3975(90)90151-7_BIB17","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1016\/0021-8693(66)90006-8","article-title":"A generalization of the functorial calculus","volume":"3","author":"Eilenberg","year":"1966","journal-title":"J. Algebra"},{"key":"10.1016\/0304-3975(90)90151-7_BIB18","series-title":"Structural polymorphism I, II, III","author":"Freyd","year":"1989"},{"key":"10.1016\/0304-3975(90)90151-7_BIB19","series-title":"Proc.v 3rd IEEE Symp. on Logic in Computer Science","article-title":"Semantic parametricity in polymorphic lambda calculus","author":"Freyd","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB20","series-title":"Second Scandinavian Logic Symposium, 1970","first-page":"63","article-title":"Une extension de l'interpr\u00e9tation de G\u00f6del","author":"Girard","year":"1971"},{"key":"10.1016\/0304-3975(90)90151-7_BIB21","series-title":"Th\u00e8se de Doctorat d'Etat","article-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"10.1016\/0304-3975(90)90151-7_BIB22","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variables types, fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90151-7_BIB23","article-title":"Edinburgh LCF","volume":"78","author":"Gordon","year":"1979"},{"key":"10.1016\/0304-3975(90)90151-7_BIB24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0022680","article-title":"Deduction and computation","author":"Huet","year":"1986"},{"key":"10.1016\/0304-3975(90)90151-7_BIB25","article-title":"A uniform approach to type theory","author":"Huet","year":"1987","journal-title":"Logical Foundations of Functional Programming, Proceedings University of Texas Programming Institute"},{"key":"10.1016\/0304-3975(90)90151-7_BIB26","year":"1987","journal-title":"Logical Foundations of Functional Programming, Proceedings University of Texas Programming Institute"},{"key":"10.1016\/0304-3975(90)90151-7_BIB27","series-title":"The L.E.J. Brouwer Centenary","article-title":"The effective topos","author":"Hyland","year":"1982"},{"key":"10.1016\/0304-3975(90)90151-7_BIB28","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(88)90018-8","article-title":"A small complete category","volume":"40","author":"Hyland","year":"1988","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/0304-3975(90)90151-7_BIB29","author":"Hyland","year":"1987","journal-title":"The discrete objects in the effective topos"},{"key":"10.1016\/0304-3975(90)90151-7_BIB30","series-title":"Technical Report 88-234","article-title":"Algebraic types in PER models","author":"Hyland","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB31","series-title":"Coherence in Categories","first-page":"66","article-title":"Many-variable function calculus I","volume":"281","author":"Kelly","year":"1977"},{"key":"10.1016\/0304-3975(90)90151-7_BIB32","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/0304-3975(90)90151-7_BIB33","article-title":"Introduction to Higher-Order Categorical Logic","volume":"7","author":"Lambek","year":"1986"},{"key":"10.1016\/0304-3975(90)90151-7_BIB34","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/365230.365257","article-title":"The next 700 programming languages","volume":"9","author":"Landin","year":"1964","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(90)90151-7_BIB35","article-title":"Clu Reference Manual","volume":"114","author":"Liskov","year":"1981"},{"key":"10.1016\/0304-3975(90)90151-7_BIB36","series-title":"Workshop on Semantics of Natural and Computer Languages","article-title":"Constructive natural deduction and its \u201cmodest\u201d interpretation","author":"Longo","year":"1987"},{"key":"10.1016\/0304-3975(90)90151-7_BIB37","article-title":"Categories for the Working Mathematician","volume":"5","author":"MacLane","year":"1971"},{"key":"10.1016\/0304-3975(90)90151-7_BIB38","series-title":"Sixth Internat. Congress of Logic, Methodology and Philosophy of Science","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/0304-3975(90)90151-7_BIB39","series-title":"Relating models of polymorphism","author":"Meseguer","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB40","first-page":"184","article-title":"A proposal for standard ML","author":"Milner","year":"1984","journal-title":"Proc. ACM Symp. on LISP and Functional Programming"},{"key":"10.1016\/0304-3975(90)90151-7_BIB41","first-page":"308","article-title":"A type-inference approach to reduction properties and semantics of polymorphic expressions","author":"Mitchell","year":"1986","journal-title":"Proc. 1986 ACM Symp. on Lisp and Functional Programming"},{"key":"10.1016\/0304-3975(90)90151-7_BIB42","first-page":"28","article-title":"The essence of ML","author":"Mitchell","year":"1988","journal-title":"Proc. 15th ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(90)90151-7_BIB43","first-page":"225","article-title":"Second-order logical relations","volume":"193","author":"Mitchell","year":"1985"},{"key":"10.1016\/0304-3975(90)90151-7_BIB44","series-title":"Proc. Symp. on Category Theory and Computer Science","article-title":"Polymorphism is set-theoretic, constructively","volume":"283","author":"Pitts","year":"1987"},{"key":"10.1016\/0304-3975(90)90151-7_BIB45","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90151-7_BIB46","first-page":"408","article-title":"Towards a theory of type structure","volume":"19","author":"Reynolds","year":"1974"},{"key":"10.1016\/0304-3975(90)90151-7_BIB47","series-title":"Algorithmic Languages","first-page":"345","article-title":"The essence of Algol.","author":"Reynolds","year":"1981"},{"key":"10.1016\/0304-3975(90)90151-7_BIB48","series-title":"Information Processing '83","first-page":"513","article-title":"Types, abstraction, and parametric polymorphism","author":"Reynolds","year":"1983"},{"key":"10.1016\/0304-3975(90)90151-7_BIB49","series-title":"Symp. on Semantics of Data Types","article-title":"Polymorphism is not set-theoretic","volume":"173","author":"Reynolds","year":"1984"},{"key":"10.1016\/0304-3975(90)90151-7_BIB50","series-title":"Research Report","article-title":"Preliminary design of the programming language Forsythe","author":"Reynolds","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB51","doi-asserted-by":"crossref","unstructured":"J.C. Reynolds and G.D. Plotkin, On functors expressible in the polymorphic typed lambda calculus, Inform. and Comput., to appear.","DOI":"10.1006\/inco.1993.1037"},{"key":"10.1016\/0304-3975(90)90151-7_BIB52","series-title":"Technical Report 88-229","article-title":"How complete is PER?","author":"Robinson","year":"1988"},{"key":"10.1016\/0304-3975(90)90151-7_BIB53","unstructured":"A. Scedrov, A guide to polymorphic types, in: P. Odifreddi, ed., Logic and Computer Science, Proc. C.I.M.E. Summer School, Montecatini Terme (June 1988), Lecture Notes in COmputer Science (Springer, Berlin, to appear)."},{"key":"10.1016\/0304-3975(90)90151-7_BIB54","series-title":"Toposes, Algebraic Geometry and Logic","first-page":"97","article-title":"Continuous lattices","volume":"274","author":"Scott","year":"1972"},{"key":"10.1016\/0304-3975(90)90151-7_BIB55","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0304-3975(90)90151-7_BIB56","series-title":"Proc. ICALP '82","article-title":"Domains for denotational semantics","volume":"140","author":"Scott","year":"1982"},{"key":"10.1016\/0304-3975(90)90151-7_BIB57","author":"Scott","year":"1987","journal-title":"Realizability and domain theory"},{"key":"10.1016\/0304-3975(90)90151-7_BIB58","doi-asserted-by":"crossref","first-page":"969","DOI":"10.2307\/2273831","article-title":"Categorical semantics for higher-order polymorphic lambda calculus","volume":"52","author":"Seely","year":"1987","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(90)90151-7_BIB59","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1137\/0211062","article-title":"The category-theoretic solution of recursive domain equations","volume":"11","author":"Smyth","year":"1982","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0304-3975(90)90151-7_BIB60","series-title":"Lecture Notes","article-title":"Fundamental concepts in programming languages","author":"Strachey","year":"1967"},{"key":"10.1016\/0304-3975(90)90151-7_BIB61","series-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","volume":"344","year":"1973"},{"key":"10.1016\/0304-3975(90)90151-7_BIB62","series-title":"Functional Programming Languages and Computer Architecture","article-title":"Miranda: a non-strict functional language with polymorphic types","volume":"201","author":"Turner","year":"1985"},{"key":"10.1016\/0304-3975(90)90151-7_BIB63","first-page":"507","article-title":"On Ext and exact sequences","volume":"8","author":"Yoneda","year":"1960","journal-title":"J. Fac. Sci. Tokyo Sec 1"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397590901517?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397590901517?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T22:25:16Z","timestamp":1555194316000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397590901517"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,1]]},"references-count":64,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,1]]}},"alternative-id":["0304397590901517"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(90)90151-7","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1990,1]]}}}