{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:52:58Z","timestamp":1760079178253},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":9598,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1987,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including \u201csubtypes\u201d, for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.<\/jats:p>","DOI":"10.2307\/2273831","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:23:41Z","timestamp":1146954221000},"page":"969-989","source":"Crossref","is-referenced-by-count":81,"title":["Categorical semantics for higher order polymorphic lambda calculus"],"prefix":"10.1017","volume":"52","author":[{"given":"R. A. G.","family":"Seely","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200029364_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80033-3"},{"key":"S0022481200029364_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061361"},{"key":"S0022481200029364_ref017","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0022481200029364_ref018","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19780243109"},{"key":"S0022481200029364_ref006","unstructured":"Girard J.-Y. [1972], Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 Paris-VII, Paris. (Much of this is summarised in Girard [1971], [1973].)"},{"key":"S0022481200029364_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700044828"},{"key":"S0022481200029364_ref003","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"S0022481200029364_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0022481200029364_ref008","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0022481200029364_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_6"},{"key":"S0022481200029364_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0022481200029364_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066776"},{"key":"S0022481200029364_ref013","volume-title":"The standard ML core language","author":"Milner","year":"1984"},{"key":"S0022481200029364_ref009","unstructured":"Lamarche F. [1985], Unpublished lecture notes, McGill University, Montr\u00e9al."},{"key":"S0022481200029364_ref010","volume-title":"Introduction to higher order categorical logic","volume":"7","author":"Lambek","year":"1986"},{"key":"S0022481200029364_ref012","unstructured":"McCracken N. J. [1979], An investigation of a programming language with a polymorphic type structure, Ph.D. Thesis, Syracuse University, Syracuse, New York."},{"key":"S0022481200029364_ref015","first-page":"408","volume-title":"Collogue sur la programmation","volume":"19","author":"Reynolds","year":"1974"},{"key":"S0022481200029364_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"S0022481200029364_ref019","volume-title":"Girard's type theory and categories","author":"Seely","year":"1979"},{"key":"S0022481200029364_ref020","first-page":"448","article-title":"Review of P. T. Johnstone","volume":"47","author":"Seely","year":"1982","journal-title":"Topos theory"},{"key":"S0022481200029364_ref021","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19830291005"},{"key":"S0022481200029364_ref024","first-page":"197","article-title":"Higher order polymorphic lambda calculus and categories. II","volume":"8","author":"Seely","year":"1986","journal-title":"Mathematical Reports of the Academy of Science (Canada)"},{"key":"S0022481200029364_ref022","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"S0022481200029364_ref023","first-page":"135","article-title":"Higher order polymorphic lambda calculus and categories. I","volume":"8","author":"Seely","year":"1986","journal-title":"Mathematical Reports of the Academy of Science (Canada)"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200029364","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T21:17:17Z","timestamp":1558387037000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.cambridge.org\/core\/product\/identifier\/S0022481200029364\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,12]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1987,12]]}},"alternative-id":["S0022481200029364"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.2307\/2273831","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,12]]}}}