{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T20:32:30Z","timestamp":1776198750171,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540190202","type":"print"},{"value":"9783540389200","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19020-1_2","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:55:01Z","timestamp":1330199701000},"page":"23-42","source":"Crossref","is-referenced-by-count":25,"title":["A categorical approach to realizability and polymorphic types"],"prefix":"10.1007","author":[{"given":"Aurelio","family":"Carboni","sequence":"first","affiliation":[]},{"given":"Peter J.","family":"Freyd","sequence":"additional","affiliation":[]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"2_CR1","unstructured":"Bainbridge E. S., Freyd P. J., Scedrov A., Scott P. J. [88], Functorial polymorphism. In: \"Logical Foundations of Functional Programming\" (G. Huet, ed.), Addison-Wesley, to appear."},{"key":"2_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of constructive mathematics","author":"M. Beeson","year":"1985","unstructured":"Beeson M. [1985], \"Foundations of constructive mathematics\". Ergeb. der Math., Springer-Verlag, New York."},{"key":"2_CR3","doi-asserted-by":"crossref","first-page":"6","DOI":"10.2307\/2273251","volume":"46","author":"A. Boileau","year":"1981","unstructured":"Boileau A., Joyal A. [1981], La logique des topos. J. Symb. Logic 46, 6\u201316.","journal-title":"J. Symb. Logic"},{"key":"2_CR4","unstructured":"Breazu-Tannen V., Coquand T. [87], Extensional models for polymorphism. Proc. TAPSOFT '87 \u2014 CFLP, Pisa, Theor. Comp. Sci., to appear."},{"key":"2_CR5","unstructured":"Bruce K. B., Meyer A. R., Mitchell J. C. [87], The semantics of second-order lambda calculus. Information & Computation, to appear."},{"key":"2_CR6","unstructured":"Carboni A., Walters R. F. C. [88], Cartesian bicategories I. J. Pure Appl. Algebra, to appear."},{"issue":"4","key":"2_CR7","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli L., Wegner P. [1985], On understanding types, data abstraction, and polymorphism. ACM Comp. Surveys 17 (4) 471\u2013522.","journal-title":"ACM Comp. Surveys"},{"key":"2_CR8","unstructured":"Cousineau G., Curien P. L., Robinet B. (eds.) [86], \"Combinators and functional programming languages\". Springer LNCS 242."},{"key":"2_CR9","unstructured":"Freyd P. J. [74], On functorializing model theory, or: on canonizing category theory. Manuscript."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0022-4049(72)90001-1","volume":"2","author":"P. J. Freyd","year":"1972","unstructured":"Freyd P. J., Kelly G. M. [1972], Categories of continuous functors I. J. Pure Appl. Alg. 2, 169\u2013191; Erratum, ibid. 4 (1974), 121.","journal-title":"J. Pure Appl. Alg."},{"key":"2_CR11","first-page":"315","volume-title":"Some semantic aspects of polymorphic lambda calculus","author":"P. J. Freyd","year":"1987","unstructured":"Freyd P. J., Scedrov, A. [1987], Some semantic aspects of polymorphic lambda calculus. Proc. 2nd IEEE Symp. Logic in Computer Science, Ithaca, N.Y., pp. 315\u2013319."},{"key":"2_CR12","series-title":"Math. Library Ser.","volume-title":"Geometric logic","author":"P. J. Freyd","year":"1988","unstructured":"Freyd P.J., Scedrov A. [1988], \"Geometric logic\". Math. Library Ser., North-Holland, Amsterdam, to appear."},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0049-237X(08)70843-7","volume-title":"Proc. 2nd Scandinavian Logic Symp","author":"J. Y. Girard","year":"1971","unstructured":"Girard J.Y. [1971], Une extension de l'interpr\u00e9tation de l'interpr\u00e9tation de G\u0151del ... Proc. 2nd Scandinavian Logic Symp. (J. Fenstad, ed.), North-Holland, Amsterdam, 63\u201392."},{"key":"2_CR14","unstructured":"Girard J.Y. [72], \"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures ...\". Th\u00e8se de Doctorat d'Etat. Universit\u00e9 Paris VII."},{"key":"2_CR15","first-page":"165","volume-title":"Proc. Brouwer Centenary Symposium","author":"J. M. E. E. Hyland","year":"1982","unstructured":"Hyland J.M.E. [1982], The effective topos. Proc. Brouwer Centenary Symposium (A. S. Troelstra, D. van Dalen, eds.), North-Holland, Amsterdam, 165\u2013216."},{"key":"2_CR16","unstructured":"Hyland J.M.E., Robinson, E., Rosolini, G. [87], Discrete objects in a topos. Preprint."},{"key":"2_CR17","first-page":"1","volume":"91","author":"S. C. Kleene","year":"1959","unstructured":"Kleene S.C. [1959], Recursive functionals and quantifiers of finite type I. Trans. Amer. Math. Soc. 91, 1\u201352.","journal-title":"Trans. Amer. Math. Soc."},{"key":"2_CR18","unstructured":"Lambek J., Scott P. [86], \"Introduction to higher-order categorical logic\". Cambridge Univ. Press."},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0168-0072(86)90050-3","volume":"32","author":"D. C. McCarty","year":"1986","unstructured":"McCarty D.C. [1986], Realizability and recursive set theory. Ann. Pure Appl. Logic 32, 153\u2013183.","journal-title":"Ann. Pure Appl. Logic"},{"key":"2_CR20","unstructured":"Mitchell J.C. [86], A type-inference approach to reduction properties and semantics of polymorphic expressions. Symp. on Lisp and Functional Programming."},{"key":"2_CR21","first-page":"408","volume":"19","author":"J. C. Reynolds","year":"1974","unstructured":"Reynolds J. C. [1974], Towards a theory of type structure. Springer LNCS 19, 408\u2013425.","journal-title":"Springer LNCS"},{"key":"2_CR22","unstructured":"Reynolds J.C. [84], Polymorphism is not set-theoretic. Springer LNCS 173."},{"key":"2_CR23","unstructured":"Rosolini G. [86], About modest sets. Preprint"},{"key":"2_CR24","unstructured":"Scedrov A. [88], Recursive realizability and the calculus of constructions. In: \"Logical Foundations of Functional Programming\" (G. Huet, ed.), Addison-Wesley, to appear."},{"key":"2_CR25","unstructured":"Scott D.S. [82], Domains for denotational semantics. ICALP 82. Springer LNCS 140."},{"key":"2_CR26","unstructured":"Seely R.A.G. [87], Categorical semanticsfor higher-order polymorphic lambda calculus. J. Symb. Logic, to appear."},{"key":"2_CR27","first-page":"1","volume":"144","author":"E. Wagner","year":"1969","unstructured":"Wagner E. [1969], Uniformly reflective structures: on the nature of g\u0151delizations and relative computability. Trans. Amer. Math. Soc. 144, 1\u201341.","journal-title":"Trans. Amer. Math. Soc."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Programming Language Semantics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19020-1_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:18:59Z","timestamp":1619558339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19020-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540190202","9783540389200"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-19020-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988]]}}}