{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:03:56Z","timestamp":1759147436804,"version":"3.44.0"},"reference-count":50,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1988,7,1]],"date-time":"1988-07-01T00:00:00Z","timestamp":583718400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1988,7,1]],"date-time":"1988-07-01T00:00:00Z","timestamp":583718400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2003,5,20]],"date-time":"2003-05-20T00:00:00Z","timestamp":1053388800000},"content-version":"vor","delay-in-days":5436,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1988,7]]},"DOI":"10.1016\/0304-3975(88)90097-7","type":"journal-article","created":{"date-parts":[[2002,10,10]],"date-time":"2002-10-10T17:44:32Z","timestamp":1034271872000},"page":"85-114","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":27,"title":["Extensional models for polymorphism"],"prefix":"10.1016","volume":"59","author":[{"given":"Val","family":"Breazu-Tannen","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(88)90097-7_BIB1","article-title":"The Lambda Calculus: Its Syntax and Semantics","volume":"103","author":"Barendregt","year":"1984"},{"key":"10.1016\/0304-3975(88)90097-7_BIB2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","article-title":"Automatic synthesis of typed \u039b-programs on term algebras","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoret. Comput. Sci."},{"journal-title":"Communication in the Types electronic forum (types@theory.lcs.mit.edu)","year":"1986","author":"Breazu-Tannen","key":"10.1016\/0304-3975(88)90097-7_BIB3"},{"key":"10.1016\/0304-3975(88)90097-7_BIB4","series-title":"Ph.D. Thesis","article-title":"Conservative extension of type theories","author":"Breazu-Tannen","year":"1987"},{"year":"1987","series-title":"Proof of a conjecture on polymorphic lambda models with all types non-empty","author":"Breazu-Tannen","key":"10.1016\/0304-3975(88)90097-7_BIB5"},{"key":"10.1016\/0304-3975(88)90097-7_BIB6","first-page":"291","article-title":"Extensional models for polymorphism","volume":"250","author":"Breazu-Tannen","year":"1987"},{"key":"10.1016\/0304-3975(88)90097-7_BIB7","first-page":"238","article-title":"Computable values can be classical","author":"Breazu-Tannen","year":"1987","journal-title":"Proc. 14th Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(88)90097-7_BIB8","first-page":"7","article-title":"Polymorphism is conservative over simple types","author":"Breazu-Tannen","year":"1987","journal-title":"Proc. Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(88)90097-7_BIB9","first-page":"131","article-title":"The semantics of second-order polymorphic lambda calculus","volume":"173","author":"Bruce","year":"1984"},{"key":"10.1016\/0304-3975(88)90097-7_BIB10","series-title":"LISP Conference","first-page":"136","article-title":"Hope: an experimental applicative language","author":"Burstall","year":"1980"},{"key":"10.1016\/0304-3975(88)90097-7_BIB11","first-page":"23","article-title":"A categorical approach to realizability and polymorphic types","volume":"298","author":"Carboni","year":"1988"},{"journal-title":"Combinators and Functional Programming Languages, Proc. 13th Summer School of the LITP, Le Val D'Ajol, France","year":"1985","author":"Cardelli","key":"10.1016\/0304-3975(88)90097-7_BIB12"},{"issue":"4","key":"10.1016\/0304-3975(88)90097-7_BIB13","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"},{"journal-title":"Communication in the Types electronic formum (types@theory.lcs.mit.edu)","year":"1986","author":"Coquand","key":"10.1016\/0304-3975(88)90097-7_BIB14"},{"key":"10.1016\/0304-3975(88)90097-7_BIB15","series-title":"Tech. Rept. 31","article-title":"Ponder and its type system","author":"Fairbairn","year":"1982"},{"issue":"1","key":"10.1016\/0304-3975(88)90097-7_BIB16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","article-title":"The expressiveness of simple and second-order type structures","volume":"30","author":"Fortune","year":"1983","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(88)90097-7_BIB17","first-page":"315","article-title":"Some semantics aspects of polymorphic lambda calculus","author":"Freyd","year":"1987","journal-title":"Proc. Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(88)90097-7_BIB18","series-title":"Proc. Logic Colloqium '73","first-page":"22","article-title":"Equality between functionals","volume":"453","author":"Friedman","year":"1975"},{"key":"10.1016\/0304-3975(88)90097-7_BIB19","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2268484","article-title":"On the axiom of extensionality\u2014Part I","volume":"21","author":"Gandy","year":"1956","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(88)90097-7_BIB20","series-title":"Ph.D. Thesis","article-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure","author":"Girard","year":"1972"},{"key":"10.1016\/0304-3975(88)90097-7_BIB21","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/947886.947887","article-title":"Completeness of many-sorted equational logic","volume":"17","author":"Goguen","year":"1982","journal-title":"SIGPLAN Notes"},{"key":"10.1016\/0304-3975(88)90097-7_BIB22","article-title":"Edinburgh LCF","volume":"78","author":"Gordon","year":"1979"},{"key":"10.1016\/0304-3975(88)90097-7_BIB23","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19800261902","article-title":"Lambda-calculus models and extensionality","volume":"26","author":"Hindley","year":"1980","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"10.1016\/0304-3975(88)90097-7_BIB24","doi-asserted-by":"crossref","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"},{"journal-title":"The discrete objects in the effective topos","year":"1987","author":"Hyland","key":"10.1016\/0304-3975(88)90097-7_BIB25"},{"key":"10.1016\/0304-3975(88)90097-7_BIB26","series-title":"Constructivity in Mathematics","first-page":"101","article-title":"Interpretation of analysis by means of constructive functionals of finite types","author":"Kreisel","year":"1959"},{"key":"10.1016\/0304-3975(88)90097-7_BIB27","first-page":"460","article-title":"Reasoning about functional programs and complexity classes associated with type disciplines","author":"Leivant","year":"1983","journal-title":"Proc. 24th Symp. on Foundations of Computer Science"},{"key":"10.1016\/0304-3975(88)90097-7_BIB28","series-title":"Tech. Rept. 63","article-title":"Poly manual","author":"Matthews","year":"1985"},{"journal-title":"Communication in the Types electronic forum (types@theory.lcs.mit.edu)","year":"1986","author":"Meyer","key":"10.1016\/0304-3975(88)90097-7_BIB29"},{"issue":"1","key":"10.1016\/0304-3975(88)90097-7_BIB30","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","article-title":"What is a model of the lambda calculus?","volume":"52","author":"Meyer","year":"1982","journal-title":"Inform. and Control"},{"key":"10.1016\/0304-3975(88)90097-7_BIB31","first-page":"253","article-title":"Empty types in polymorphic \u03bb-calculus","author":"Meyer","year":"1987","journal-title":"Proc. 14th Symp. on Principles of Programming Languages"},{"journal-title":"Personal communication","year":"1986","author":"Mitchell","key":"10.1016\/0304-3975(88)90097-7_BIB32"},{"key":"10.1016\/0304-3975(88)90097-7_BIB33","first-page":"308","article-title":"A type-inference approach to reduction properties and semantics of polymorphic expressions","author":"Mitchell","year":"1986","journal-title":"Proc. LISP and Functional Programming Conf.,"},{"key":"10.1016\/0304-3975(88)90097-7_BIB34","first-page":"225","article-title":"Second-order logical relations (extended abstract)","volume":"193","author":"Mitchell","year":"1985"},{"key":"10.1016\/0304-3975(88)90097-7_BIB35","first-page":"303","article-title":"Kripke-style models for typed lambda calculus","author":"Mitchell","year":"1987","journal-title":"Proc. Symp. on Logic in Computer Science"},{"journal-title":"Communication in the Types electronic forum (types@theory.lcs.mit.edu)","year":"1986","author":"Moggi","key":"10.1016\/0304-3975(88)90097-7_BIB36"},{"journal-title":"Communication in the Types electronic forum (types@theory.lcs.mit.edu)","year":"1986","author":"Moggi","key":"10.1016\/0304-3975(88)90097-7_BIB37"},{"key":"10.1016\/0304-3975(88)90097-7_BIB38","series-title":"Ph.D. Thesis","article-title":"An incremental, strongly typed database query language","author":"Nikhil","year":"1984"},{"key":"10.1016\/0304-3975(88)90097-7_BIB39","series-title":"Rept. 2\u29f887","article-title":"Polymorphisms is set theoretic, constructively","author":"Pitts","year":"1987"},{"key":"10.1016\/0304-3975(88)90097-7_BIB40","series-title":"Mathematical Foundations of Software Development","first-page":"97","article-title":"Three approaches to type structure","volume":"185","author":"Reynolds","year":"1985"},{"key":"10.1016\/0304-3975(88)90097-7_BIB41","series-title":"Programming Symp.","first-page":"408","article-title":"Towards a theory of type structure","volume":"19","author":"Reynolds","year":"1974"},{"key":"10.1016\/0304-3975(88)90097-7_BIB42","series-title":"Information Processing '83","first-page":"513","article-title":"Types, abstraction, and parametric polymorphism","author":"Reynolds","year":"1983"},{"issue":"4","key":"10.1016\/0304-3975(88)90097-7_BIB43","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"},{"issue":"2","key":"10.1016\/0304-3975(88)90097-7_BIB44","first-page":"135","article-title":"Higher-order polymorphic lambda calculus and categories","volume":"VIII","author":"Seely","year":"1986","journal-title":"Math. Rep. Acad. Sci. (Canad.)"},{"key":"10.1016\/0304-3975(88)90097-7_BIB45","doi-asserted-by":"crossref","first-page":"17","DOI":"10.2307\/2273377","article-title":"Completeness, invariance and \u03bb-definability","volume":"47","author":"Statman","year":"1982","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(88)90097-7_BIB46","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF02023009","article-title":"\u03bb-definable functionals and \u03b2\u03b7 conversion","volume":"23","author":"Statman","year":"1983","journal-title":"Arch. Math. Logik"},{"key":"10.1016\/0304-3975(88)90097-7_BIB47","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/SFCS.1981.24","article-title":"Number-theoric functions computable by polymorphic programs","author":"Statman","year":"1981","journal-title":"Proc. 22nd Symp. Foundations of Computer Science"},{"key":"10.1016\/0304-3975(88)90097-7_BIB48","series-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","first-page":"511","article-title":"On the existence of closed terms in the typed \u03bb-calculus","author":"Statman","year":"1980"},{"volume":"344","year":"1973","series-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","key":"10.1016\/0304-3975(88)90097-7_BIB49"},{"key":"10.1016\/0304-3975(88)90097-7_BIB50","series-title":"Proc. conf. on Functional Programming Languages and Computer Architecture","first-page":"1","article-title":"Miranda: a nonstrict functional language with polymorphic types","volume":"201","author":"Turner","year":"1985"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397588900977?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397588900977?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T04:18:38Z","timestamp":1757477918000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397588900977"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,7]]},"references-count":50,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1988,7]]}},"alternative-id":["0304397588900977"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(88)90097-7","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[1988,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Extensional models for polymorphism","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/0304-3975(88)90097-7","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1988 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}