{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:22:46Z","timestamp":1779315766704,"version":"3.51.4"},"reference-count":42,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,3,1]],"date-time":"1991-03-01T00:00:00Z","timestamp":667785600000},"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":8174,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[1991,3]]},"DOI":"10.1016\/0890-5401(91)90074-c","type":"journal-article","created":{"date-parts":[[2004,12,16]],"date-time":"2004-12-16T20:34:26Z","timestamp":1103229266000},"page":"55-85","source":"Crossref","is-referenced-by-count":47,"title":["Recursion over realizability structures"],"prefix":"10.1016","volume":"91","author":[{"given":"Roberto M.","family":"Amadio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0890-5401(91)90074-C_BIB1","series-title":"3rd IEEE LICS, Edinburgh","article-title":"A fixed point extension of the second order lambda calculus: Observable equivalences and models","author":"Amadio","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB2","author":"Amadio","year":"1989"},{"key":"10.1016\/0890-5401(91)90074-C_BIB3","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0304-3975(80)90045-6","article-title":"Metric interpretation of infinite trees and semantics of non-deterministic recursive programs","volume":"11","author":"Arnold","year":"1980","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(91)90074-C_BIB4","author":"Asperti","year":"1990"},{"key":"10.1016\/0890-5401(91)90074-C_BIB5","doi-asserted-by":"crossref","first-page":"7","DOI":"10.4064\/fm-3-1-133-181","article-title":"Sur les operations dans les ensembles abstraits et leurs applications aux equations integrales","volume":"3","author":"Banach","year":"1922","journal-title":"Fund. Math."},{"key":"10.1016\/0890-5401(91)90074-C_BIB6","author":"Barendregt","year":"1984"},{"key":"10.1016\/0890-5401(91)90074-C_BIB7","doi-asserted-by":"crossref","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\/0890-5401(91)90074-C_BIB8","series-title":"3rd IEEE LICS, Edinburgh","article-title":"Modest models for inheritance and explicit polymorphism","author":"Bruce","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB9","series-title":"Semantics of Data Types","article-title":"The semantics of second order polymorhic lambda-calculus","volume":"Vol. 173","author":"Bruce","year":"1984"},{"key":"10.1016\/0890-5401(91)90074-C_BIB10","series-title":"3rd ACM Symp. on Math. Found. of Lang. Semantics","article-title":"A categorical approach to realizability and polymorphic types","author":"Carboni","year":"1987"},{"key":"10.1016\/0890-5401(91)90074-C_BIB11","series-title":"EEC Jumelage Meeting in Nijmegen","article-title":"Recursive types for fun, lecture","author":"Cardone","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB12","series-title":"Proceedings, ACM-POPL '84","article-title":"Types as intervals","author":"Cartwright","year":"1984"},{"key":"10.1016\/0890-5401(91)90074-C_BIB13","series-title":"Proceedings, 12th ICALP","article-title":"A completeness theorem for recursively defined types","volume":"Vol. 194","author":"Coppo","year":"1985"},{"key":"10.1016\/0890-5401(91)90074-C_BIB14","series-title":"1st IEEE LICS, Boston","article-title":"Type inference and logical relations","author":"Coppo","year":"1986"},{"key":"10.1016\/0890-5401(91)90074-C_BIB15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","article-title":"Fundamental properties of infinite trees","volume":"25","author":"Courcelle","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(91)90074-C_BIB16","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0890-5401(89)90068-0","article-title":"Domain theoretic models of polymorphism","volume":"81","author":"Coquand","year":"1989","journal-title":"Inform. and Comput."},{"key":"10.1016\/0890-5401(91)90074-C_BIB17","series-title":"2nd Scandinavian Logic Simposium","first-page":"63","article-title":"Une extension de l'interpretation de G\u00f6del a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types","author":"Girard","year":"1971"},{"key":"10.1016\/0890-5401(91)90074-C_BIB18","author":"Hayashi","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB19","series-title":"Technical Report","article-title":"A note on inconsistencies caused by fix-points in cartesian closed category","author":"Huwig","year":"1986"},{"key":"10.1016\/0890-5401(91)90074-C_BIB20","series-title":"Brouwer Symposium","article-title":"The effective topos","author":"Hyland","year":"1982"},{"key":"10.1016\/0890-5401(91)90074-C_BIB21","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\/0890-5401(91)90074-C_BIB22","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0890-5401(91)90074-C_BIB23","series-title":"Constructivity in Mathematics","article-title":"Interpretation of analysis by means of constructive functionals of finite type","author":"Kreisel","year":"1959"},{"key":"10.1016\/0890-5401(91)90074-C_BIB24","author":"Longo","year":"1988","journal-title":"Constructive Natural Deduction and Its Modest Interpretation"},{"key":"10.1016\/0890-5401(91)90074-C_BIB25","author":"MacLane","year":"1972"},{"key":"10.1016\/0890-5401(91)90074-C_BIB26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(86)80019-5","article-title":"An ideal model for recursive polymorphic types","volume":"71","author":"MacQueen","year":"1986","journal-title":"Inform. and Control"},{"key":"10.1016\/0890-5401(91)90074-C_BIB27","series-title":"Proceedings, Category Theory and Computer Science Conf.","article-title":"An interval model for the second order lambda-calculus","volume":"Vol. 283","author":"Martini","year":"1987"},{"key":"10.1016\/0890-5401(91)90074-C_BIB28","article-title":"Realizability and Recursive Mathematics","author":"McCarty","year":"1984","journal-title":"Ph.D. thesis"},{"key":"10.1016\/0890-5401(91)90074-C_BIB29","article-title":"Inductive Definition in Type Theory","author":"Mendler","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB30","series-title":"Lisp and Functional Programming Conference","article-title":"A type-inference approach to reduction properties and semantics of polymorphic expressions","author":"Mitchell","year":"1986"},{"key":"10.1016\/0890-5401(91)90074-C_BIB31","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","article-title":"Polymorphic type inference and containment","volume":"76","author":"Mitchell","year":"1988","journal-title":"Inform. and Comput."},{"key":"10.1016\/0890-5401(91)90074-C_BIB32","series-title":"Interpretation of second order lambda-calculus in categories","author":"Moggi","year":"1986"},{"key":"10.1016\/0890-5401(91)90074-C_BIB33","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/0890-5401(88)90010-7","article-title":"Partial morphisms in categories of effective objects","volume":"76","author":"Moggi","year":"1988","journal-title":"Inform. and Comput."},{"key":"10.1016\/0890-5401(91)90074-C_BIB34","author":"Moschovakis","year":"1974"},{"key":"10.1016\/0890-5401(91)90074-C_BIB35","first-page":"408","article-title":"Towards a theory of type structure","volume":"Vol. 19","author":"Reynolds","year":"1974"},{"key":"10.1016\/0890-5401(91)90074-C_BIB36","series-title":"Toposes, Algebraic Geometry and Logic","first-page":"97","article-title":"Continuous lattices","volume":"Vol. 274","author":"Scott","year":"1972"},{"key":"10.1016\/0890-5401(91)90074-C_BIB37","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\/0890-5401(91)90074-C_BIB38","first-page":"4","article-title":"Categorical semantics for higher order polymorphic lambda calculus","volume":"52","author":"Seely","year":"1988","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0890-5401(91)90074-C_BIB39","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\/0890-5401(91)90074-C_BIB40","article-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","volume":"Vol. 344","author":"Troelstra","year":"1973"},{"key":"10.1016\/0890-5401(91)90074-C_BIB41","author":"Troelstra","year":"1988"},{"key":"10.1016\/0890-5401(91)90074-C_BIB42","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0304-3975(79)90053-7","article-title":"Fixed point constructions in order enriched categories","volume":"8","author":"Wand","year":"1979","journal-title":"Theoret. Comput. Sci."}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:089054019190074C?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:089054019190074C?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,31]],"date-time":"2019-01-31T01:25:45Z","timestamp":1548897945000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/089054019190074C"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,3]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,3]]}},"alternative-id":["089054019190074C"],"URL":"https:\/\/doi.org\/10.1016\/0890-5401(91)90074-c","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[1991,3]]}}}