{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:36:14Z","timestamp":1723487774516},"reference-count":115,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"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":4672,"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":[[2000,10]]},"DOI":"10.1016\/s0304-3975(00)00057-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:32:20Z","timestamp":1027593140000},"page":"81-161","source":"Crossref","is-referenced-by-count":35,"title":["From computation to foundations via functions and application: The \u03bb-calculus and its webbed models"],"prefix":"10.1016","volume":"249","author":[{"given":"Chantal","family":"Berline","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00057-8_BIB1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","article-title":"Domain theory in logical form","volume":"51","author":"Abramsky","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB2","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1006\/inco.1993.1044","article-title":"Full abstraction in the lazy lambda-calculus","volume":"105","author":"Abramsky","year":"1993","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB3","unstructured":"F. Alessi, Sistemi di informazione applicativi, teoria dei domini e modelli del \u03bb_calculo, Tesi di Dottorato di Ricerca in Informatica, Universit\u00e0 di Milano e Torino, 1990."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB4","doi-asserted-by":"crossref","unstructured":"F. Alessi, Type preorders, Trees in Algebra and Programming, CAAP\u201994 (Edinburg), Lecture Notes in Computer Science, Vol. 787, Springer, Berlin, 1994, pp. 37\u201351.","DOI":"10.1007\/BFb0017472"},{"issue":"8","key":"10.1016\/S0304-3975(00)00057-8_BIB5","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1145\/359576.359579","article-title":"Can programming be liberated from the von Neumann style?, A functional Style and its algebra of programs","volume":"21","author":"Backus","year":"1978","journal-title":"Comm. ACM (Association of Computing Machinery)"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB6","doi-asserted-by":"crossref","unstructured":"J. Baeten, B. Boerboom, Omega can be anything it should not be, Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Serie A, Indag. Mathematicae, Vol. 41, 1979, pp. 111\u2013120.","DOI":"10.1016\/1385-7258(79)90016-7"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB7","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","article-title":"Complete restrictions of the intersection type discipline","volume":"102","author":"van Bakel","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB8","series-title":"The Lambda-Calculus, its Syntax and Semantics, revised ed. Studies in Logic, Vol. 103","author":"Barendregt","year":"1984"},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB9","doi-asserted-by":"crossref","first-page":"181","DOI":"10.2307\/421013","article-title":"The impact of the \u03bb-calculus in logic and computer science","volume":"3","author":"Barendregt","year":"1997","journal-title":"Bull. Symbolic Logic"},{"issue":"4","key":"10.1016\/S0304-3975(00)00057-8_BIB10","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","article-title":"A filter model and the completeness of type assignment","volume":"48","author":"Barendregt","year":"1983","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB11","unstructured":"O. Bastonero, Mod\u00e8les fortement stables du \u03bb-calcul et r\u00e9sultats d'incompl\u00e9tude, Th\u00e8se, Universit\u00e9 de Paris 7, December 1996."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB12","unstructured":"O. Bastonero, Equational incompleteness and incomparability results for \u03bb-calculus semantics, J. Symbolic Logic, submitted."},{"issue":"10","key":"10.1016\/S0304-3975(00)00057-8_BIB13","first-page":"905","article-title":"Stabilit\u00e9 forte et incompl\u00e9tude de la classe des mod\u00e8les stables du \u03bb-calcul","volume":"322","author":"Bastonero","year":"1996","journal-title":"Notes C.-R. Acad. Sci. S\u00e9r. I"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB14","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/S0168-0072(99)00015-9","article-title":"Strong stability and the incompleteness of stable models of \u03bb-calculus","volume":"100","author":"Bastonero","year":"1999","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB15","article-title":"Infinite \u03bb-calculus and non-sensible models","volume":"Vol. 180","author":"Berarducci","year":"1996"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB16","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0304-3975(98)00135-2","article-title":"Infinite \u03bb-calculus and Types","volume":"212","author":"Berarducci","year":"1999","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB17","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(93)90084-7","article-title":"Some new results on easy \u03bb-terms","volume":"121","author":"Berarducci","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB18","doi-asserted-by":"crossref","unstructured":"S. Berardi, C. Berline, Building continuous webbed models for System F, preprint October 1998, to appear in ENTCS (2000).","DOI":"10.1016\/S1571-0661(05)01195-3"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB19","doi-asserted-by":"crossref","unstructured":"C. Berline, K. Grue, A kappa-denotational semantics for Map Theory, in ZFC+SI, Theoret. Comput. Sci. 179 (1997) 137\u2013202 (the index, accidently cut at publication, Theoret. Comput. Sci. 211 (1999) 397\u2013398).","DOI":"10.1016\/S0304-3975(98)00107-8"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB20","doi-asserted-by":"crossref","unstructured":"G. Berry, Stable models of Typed \u03bb-calculi, Proc. 5th Internat. Coll. on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 62, Springer, Berlin, 1978, pp. 72\u201389.","DOI":"10.1007\/3-540-08860-1_7"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB21","unstructured":"G. Berry, Mod\u00e8les compl\u00e8tement ad\u00e9quats et stables des \u03bb-calculs typ\u00e9s, Th\u00e8se de Doctorat d\u2019\u00e9tat, Universit\u00e9 de Paris 7, 1979."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB22","unstructured":"C. B\u00f6hm, Alcune propriet\u00e0 delle forme \u03b2\u03b7-normali nel \u03bb-K-calcolo, Publicazioni dell'Istituto per le Applicazioni del Calcolo 696, Roma, 1968, 19p."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB23","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1006\/inco.1994.1003","article-title":"Lambda-calculi for (strict) parallel functions","volume":"108","author":"Boudol","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB24","unstructured":"A. Bucciarelli, Sequential models of PCF: some contributions to the domain theoretic approach to full abstraction, Dottorato di Ricerca in Informatica, Universit\u00e0 di Pisa-Genova-Udine, 1993."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB25","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(93)90005-E","article-title":"A theory of sequentiality","volume":"113","author":"Bucciarelli","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB26","doi-asserted-by":"crossref","first-page":"346","DOI":"10.2307\/1968337","article-title":"A set of postulates for the foundations of logic I","volume":"33","author":"Church","year":"1932","journal-title":"Ann. Math."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB27","doi-asserted-by":"crossref","first-page":"839","DOI":"10.2307\/1968702","article-title":"A set of postulates for the foundations of logic II","volume":"34","author":"Church","year":"1933","journal-title":"Ann. Math."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB28","unstructured":"A. Church, Lecture notes on mathematical logic Oct.35\u2013Janv.36, Princeton University, manuscript, 1936."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB29","series-title":"The calculi of \u03bb-conversion","author":"Church","year":"1941"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB30","doi-asserted-by":"crossref","unstructured":"M. Coppo, M. Dezani-Ciancaglini, G. Longo, Applicative Info. Systems, Lecture Notes in Computer Science, Vol. 159, Springer, Berlin, 1983, pp. 35\u201364.","DOI":"10.1007\/3-540-12727-5_2"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB31","series-title":"To H.B. Curry, Essays in Combinatory Logic, \u03bb-Calculus and Formalism","first-page":"535","article-title":"Principal type schemes and \u03bb-calculus semantics","author":"Coppo","year":"1980"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB32","series-title":"Logic Colloquium\u201982","first-page":"241","article-title":"Extended type structures and filter \u03bb-models","author":"Coppo","year":"1984"},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB33","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0890-5401(87)90042-3","article-title":"Type theories, normal forms and D\u221e lambda models","volume":"72","author":"Coppo","year":"1987","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB34","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","article-title":"Functionality in combinatory logic","volume":"20","author":"Curry","year":"1934","journal-title":"Proc. Natl. Acad. Sci. USA"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB35","series-title":"Every unsolvable \u03bb-term admits a decoration, preprint Juillet 98, Proc. TLCA\u201999","volume":"Vol. 1581","author":"David","year":"1999"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB36","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0304-3975(97)00004-2","article-title":"A syntactical proof of the operational equivalence of two \u03bb-terms","volume":"180","author":"David","year":"1997","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB37","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0304-3975(97)00038-8","article-title":"A decidable canonical representation of the compact elements in Scott's reflexive domain in P\u03c9","volume":"193","author":"Drakengren","year":"1998","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB38","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(86)90043-5","article-title":"A characterization of F-complete type assignments","volume":"45","author":"Dezani-Ciancaglini","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB39","doi-asserted-by":"crossref","unstructured":"P. Di Gianantonio, F. Honsell, An abstract notion of application, in TLCA\u201993, Lecture Notes in Computer Science, Vol. 664, Springer, Berlin, 1993, pp. 124\u2013138.","DOI":"10.1007\/BFb0037102"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB40","first-page":"126","article-title":"Uncountable limits and the \u03bb-calculus","volume":"2","author":"Di Gianantonio","year":"1995","journal-title":"Nordic J. Comput."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB41","first-page":"149","article-title":"Operational, denotational and logical descriptions: a case study","volume":"XVI","author":"Egidi","year":"1992","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB42","series-title":"Advances in Linear Logic, London Mathematical Society","first-page":"83","article-title":"Hypercoherences: a strongly model of linear logic","volume":"Vol. 222","author":"Ehrhard","year":"1995"},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB43","first-page":"289","article-title":"Algebras and combinators","volume":"13","author":"Engeler","year":"1981","journal-title":"Algebra Univ."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB44","doi-asserted-by":"crossref","first-page":"75","DOI":"10.2307\/2274093","article-title":"Towards useful type-free theories I","volume":"49","author":"Feferman","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB45","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0168-0072(89)90026-2","article-title":"A type-free system extending ZFC","volume":"43","author":"Flagg","year":"1989","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB46","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\/S0304-3975(00)00057-8_BIB47","series-title":"Proc. 2nd Scandinavian Logic Symp.","first-page":"63","article-title":"Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse","author":"Girard","year":"1971"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB48","unstructured":"J.Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'Arithm\u00e9tique d'ordre sup\u00e9rieure, Th\u00e8se, Universit\u00e9 Paris 7, 1972."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB49","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variable types, fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB50","series-title":"Proofs and Types, Cambridge tracts in Computer Science, Vol. 7","author":"Girard","year":"1989"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB51","unstructured":"X. Gouy, Etude des th\u00e9ories \u00e9quationnelles et des propri\u00e9t\u00e9s alg\u00e9briques des mod\u00e8les stables du \u03bb-calcul, Th\u00e8se, Universit\u00e9 de Paris 7, December 1995."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB52","first-page":"419","article-title":"Une extension du th\u00e9or\u00e8me de Hyland et Wadsworth \u00e0 une classe de mod\u00e8les du \u03bb-calcul pur","volume":"322","author":"Gouy","year":"1996","journal-title":"Notes C.-R. Acad. Sci. S\u00e9r. I"},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB53","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1006\/inco.1995.1089","article-title":"Universal retractions on DI-domains","volume":"119","author":"Gouy","year":"1995","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/S0304-3975(00)00057-8_BIB54","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(92)90296-R","article-title":"Map Theory","volume":"102","author":"Grue","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB55","unstructured":"J. van Heijenoort, From Frege to G\u00f6del, A Source Book in Mathematical Logic 1879-1931, Harvard Univ. Press, Cambridge, MA, 1967, 3rd ed. 1977."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB56","series-title":"Proc. 18th Symp. on MFCS\u201993 (Poland)","first-page":"84","article-title":"Some results on the Full Abstraction problem for Restricted Lambda Calculi","volume":"Vol. 711","author":"Honsell","year":"1993"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB57","doi-asserted-by":"crossref","unstructured":"F. Honsell, M. Lenisa, Final semantics for untyped \u03bb-calculus, TLCA\u201995, Lecture Notes in Computer Science, Vol. 902, Springer, Berlin, 1995, pp. 249\u2013265.","DOI":"10.1007\/BFb0014057"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB58","series-title":"Proc. IFIP Conf. on Programming concepts and methods","article-title":"Reasoning about interpretations in qualitative \u03bb-models","author":"Honsell","year":"1990"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB59","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-0000(92)90040-P","article-title":"An approximation theorem for topological \u03bb-models and the topological incompleteness of \u03bb-calculus","volume":"45","author":"Honsell","year":"1992","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB60","series-title":"Introduction to Combinators and \u03bb-Calculus","author":"Hindley","year":"1986"},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB61","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1112\/jlms\/s2-12.3.361","article-title":"A syntactic characterization of the equality in some models for the lambda-calculus","volume":"12","author":"Hyland","year":"1976","journal-title":"J. London Math. Soc."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB62","article-title":"A condition for identifying two elements in whatever model of combinatory logic","volume":"Vol. 37","author":"Jacopini","year":"1975"},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB63","first-page":"225","article-title":"Easy terms in the lambda-calculus","author":"Jacopini","year":"1985","journal-title":"Ann. Soc. Math. Polonae, Ser. IV; Fund. Inform. VIII"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB64","unstructured":"Y. Jiang, Consistance et inconsistance de th\u00e9ories de \u03bb-calcul \u00e9tendus, Th\u00e8se, Universit\u00e9 Paris 7, Juin 1993."},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB65","first-page":"79","article-title":"Consistency of a \u03bb-theory with n-tuples and easy terms","volume":"34","author":"Jiang","year":"1995","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB66","first-page":"587","article-title":"2\u21350 mod\u00e8les de graphes non \u00e9quationnellement \u00e9quivalents","volume":"318","author":"Kerth","year":"1994","journal-title":"Notes C.-R. Acad. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB67","first-page":"685","article-title":"D\u00e9finissabilit\u00e9 dans les domaines r\u00e9flexifs","volume":"318","author":"Kerth","year":"1994","journal-title":"Notes C.-R. Acad. Sci. S\u00e9r. I"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB68","unstructured":"R. Kerth, Isomorphisme et \u00e9quivalence \u00e9quationnelle entre mod\u00e8les du \u03bb-calcul, Th\u00e8se, Universit\u00e9 de Paris 7, October 1995."},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB69","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/A:1005018121791","article-title":"Isomorphism and equational equivalence of continuous \u03bb-models","volume":"61","author":"Kerth","year":"1998","journal-title":"Studia Logica"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB70","doi-asserted-by":"crossref","first-page":"1529","DOI":"10.2307\/2586665","article-title":"The interpretation of unsolvable terms in models of pure \u03bb-calculus","volume":"63","author":"Kerth","year":"1998","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB71","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0019-3577(99)80005-6","article-title":"Forcing in stable models of untyped \u03bb-calculus","volume":"10","author":"Kerth","year":"1999","journal-title":"Indagationes Mathematicae"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB72","doi-asserted-by":"crossref","unstructured":"R. Kerth, On the construction of stable models of untyped \u03bb-calculus, Theoret. Comput. Sci., submitted.","DOI":"10.1016\/S0304-3975(00)00371-6"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB73","doi-asserted-by":"crossref","unstructured":"S.C. Kleene, Realizability: a retrospective survey, Proc. Cambridge Summer School in Mathematical Logic, Cambridge 1971, Lecture Notes in Mathematics, Vol, 337, Springer, Berlin, 1973, pp. 95\u2013112.","DOI":"10.1007\/BFb0066772"},{"issue":"1","key":"10.1016\/S0304-3975(00)00057-8_BIB74","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/MAHC.1981.10004","article-title":"Origins of recursive function theory","volume":"3","author":"Kleene","year":"1981","journal-title":"Ann. History Comput."},{"issue":"2","key":"10.1016\/S0304-3975(00)00057-8_BIB75","doi-asserted-by":"crossref","first-page":"630","DOI":"10.2307\/1968646","article-title":"The inconsistency of certain formal logics","volume":"36","author":"Kleene","year":"1935","journal-title":"Ann. Math."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB76","series-title":"Lambda-calcul, Types et mod\u00e8les","author":"Krivine","year":"1990"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB77","unstructured":"J.L. Krivine, Lambda-Calculus, Types and Models, Ellis-Horwood, Chichester, 1993. (augmented english translation of the above)."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB78","first-page":"63","article-title":"Fonctions, Programmes et D\u00e9monstrations","volume":"60","author":"Krivine","year":"1994","journal-title":"Gaz. Math. Soc. Math. Fr."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB79","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0168-0072(94)90047-7","article-title":"Classical logic, storage operators and second-order lambda-calculus","volume":"68","author":"Krivine","year":"1994","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB80","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF02127805","article-title":"About classical logic and imperative programming","volume":"16","author":"Krivine","year":"1996","journal-title":"Ann. Math. Artificial Intelligence"},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB81","first-page":"149","article-title":"Programming with proofs","volume":"26","author":"Krivine","year":"1990","journal-title":"J. Inform. Process. Cybernet. EIK"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB82","series-title":"Set Theory, An Introduction to Independence proofs","volume":"Vol. 102","author":"Kunen","year":"1964"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB83","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","article-title":"The mechanical evaluation of expressions","volume":"6","author":"Landin","year":"1964","journal-title":"Comput. J."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB84","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, G. Winskel, Using Information Systems to Solve Recursive Domain Equations, Lecture Notes in Computer Science, Vol. 173, (Semantics of data types), Springer, Berlin, 1984, pp. 109\u2013130.","DOI":"10.1007\/3-540-13346-1_5"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB85","first-page":"460","article-title":"Reasoning about functional programs and complexity classes associated with type discipline","author":"Leivant","year":"1983","journal-title":"24th Annual Symp. on Foundations of Computer Science"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB86","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(83)90030-1","article-title":"Set-theoretical models of \u03bb-calculus: theories, expansions and isomorphisms","volume":"24","author":"Longo","year":"1983","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB87","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","article-title":"Petri nets, event structures and domains (part I)","volume":"13","author":"Nielsen","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB88","series-title":"Classical Recursion Theory, Studies in Mathematical Logic, Vol. 125","author":"Odifreddi","year":"1989"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB89","series-title":"Logic in Computer Science","first-page":"1","article-title":"Introduction","volume":"Vol. 31","author":"Odifreddi","year":"1990"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB90","doi-asserted-by":"crossref","unstructured":"M. Parigot, On the representations of data in lambda-calculus, in Proc. CSL\u201989 (Kaiserlautern), Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1989, pp. 309\u2013321.","DOI":"10.1007\/3-540-52753-2_47"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB91","doi-asserted-by":"crossref","unstructured":"M. Parigot, P. Roziere, Constant time reduction in \u03bb-calculus, Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 711, Springer, Berlin, 1993, pp. 608\u2013617.","DOI":"10.1007\/3-540-57182-5_52"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB92","unstructured":"D. Park, The Y combinator in Scott's Lambda-calculus models. Theory of Computation Report 13, Department of Computer Science, University of Warwick, 1976."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB93","unstructured":"G. Plotkin, A set-theoretical definition of application, Memorandum MIP-R-95, School of artificial intelligence, University of Edinburgh, 1972."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB94","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the \u03bb-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB95","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB96","unstructured":"G.D. Plotkin, Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa notes\u201d, Department of Computer Science, University of Edinburgh, 1981."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB97","doi-asserted-by":"crossref","unstructured":"G. Plotkin, A power domain for countable non-determinism. Lecture Notes in Computer Science, Vol. 140, ICALP\u201982, Springer, Berlin, 1982, pp. 418\u2013428.","DOI":"10.1007\/BFb0012788"},{"issue":"1\u20132","key":"10.1016\/S0304-3975(00)00057-8_BIB98","first-page":"159","article-title":"Set-Theoretical and other elementary models of the \u03bb-calculus (in a collection of contributions in honour to Corrado B\u00f6hm on the occasion of his 70th birthday)","volume":"121","author":"Plotkin","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB99","doi-asserted-by":"crossref","unstructured":"G. Plotkin, A semantic for static type inference, Inform. and Comput. 109 (1\u20132) (1994) pp. 256\u2013299. (Special issue TACS\u201991).","DOI":"10.1006\/inco.1994.1018"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB100","unstructured":"G. Plotkin, On a question of Friedman, preprint, 1995."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB101","doi-asserted-by":"crossref","unstructured":"J. Reynolds, Toward a theory of type structures, Colloque sur la programmation, Lecture Notes in Computer Science, Vol. 19, Springer, Berlin, 1974, pp. 408\u2013425.","DOI":"10.1007\/3-540-06859-7_148"},{"issue":"1","key":"10.1016\/S0304-3975(00)00057-8_BIB102","doi-asserted-by":"crossref","first-page":"227","DOI":"10.2307\/2274916","article-title":"Isomorphisms and non isomorphisms of graph models","volume":"56","author":"Schellinx","year":"1991","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB103","series-title":"Lecture Notes in Mathematics, Vol. 274, Topos, Algebraic geometry and Logic, Proc. Dalhousie Conf.","first-page":"97","article-title":"Continuous lattices","author":"Scott","year":"1972"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB104","series-title":"\u03bb-Calculus and Computer Science Theory, Lecture Notes in Computer Science, Vol. 37","article-title":"Some philosophical issues concerning the theory of combinators","author":"Scott","year":"1975"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB105","series-title":"\u03bb-Calculus and Computer Science Theory","first-page":"1","article-title":"Combinators and classes","volume":"Vol. 37","author":"Scott","year":"1975"},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB106","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\/S0304-3975(00)00057-8_BIB107","series-title":"The Kleene Symp.","first-page":"223","article-title":"Lambda-calculus: some models, some philosophy","author":"Scott","year":"1980"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB108","series-title":"Ordered Sets, Proc. NATO Advanced Study Institute, (Banff, Canada 1981)","first-page":"677","article-title":"Some ordered sets in computer science","author":"Scott","year":"1981"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB109","doi-asserted-by":"crossref","unstructured":"D. Scott, Domains for denotational semantics, Lecture Notes in Computer Science, Vol. 140, (ICALP\u201982) Springer, Berlin, 1982, pp. 577\u2013613.","DOI":"10.1007\/BFb0012801"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB110","first-page":"422","author":"Selinger","year":"1996","journal-title":"Order-incompleteness and finite lambda-models, in Proc. 11th Annual IEEE Symp. on Logic and Computer Science (LICS\u201996)"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB111","unstructured":"J. Stoy, Denotational semantics: the Scott-Strachey approach to Programming language Theory, MIT Press Series in Computer Science, 3rd printing, 1985."},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB112","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The relation between computational and denotational properties for Scott's D\u221e-models of \u03bb-calculus","volume":"5","author":"Wadsworth","year":"1976","journal-title":"SIAM J. Comput."},{"issue":"3","key":"10.1016\/S0304-3975(00)00057-8_BIB113","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1137\/0207028","article-title":"Approximate reduction and \u03bb-calculus models","volume":"7","author":"Wadsworth","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0304-3975(00)00057-8_BIB114","series-title":"An introduction to event structures, Lecture notes for the REX Summer School in Temporal Logic","volume":"Vol. 354","author":"Winskel","year":"1988"},{"key":"10.1016\/S0304-3975(00)00057-8_BIB115","unstructured":"C. Zylberajch, Syntaxe et s\u00e9mantique de la facilit\u00e9 en \u03bb-calcul, Th\u00e8se, Universit\u00e9 Paris 7, 1991."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000578?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000578?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T06:41:10Z","timestamp":1578552070000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500000578"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":115,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["S0304397500000578"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00057-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}