{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T19:52:38Z","timestamp":1673725958941},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,10,31]],"date-time":"2007-10-31T00:00:00Z","timestamp":1193788800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,4]]},"DOI":"10.1007\/s00224-007-9079-5","type":"journal-article","created":{"date-parts":[[2007,10,30]],"date-time":"2007-10-30T20:09:19Z","timestamp":1193774959000},"page":"306-348","source":"Crossref","is-referenced-by-count":6,"title":["Logical Equivalence for Subtyping Object and Recursive Types"],"prefix":"10.1007","volume":"42","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[]},{"given":"Ugo","family":"de\u2019Liguoro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,10,31]]},"reference":[{"key":"9079_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Berlin (1996)"},{"key":"9079_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/BFb0030634","volume-title":"Proc. of TAPSOFT \u201997","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Leino, K.: A logic of object oriented programs. In: Proc. of TAPSOFT \u201997. Lecture Notes in Computer Science, vol.\u00a01214, pp.\u00a0682\u2013696. Springer, Berlin (1997)"},{"key":"9079_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Plotkin, G.D.: A per model of polymorphism and recursive types. In: Proc. of LICS\u201990, pp.\u00a0355\u2013365 (1990)","DOI":"10.1109\/LICS.1990.113761"},{"key":"9079_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","volume":"51","author":"S. Abramsky","year":"1991","unstructured":"Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Log. 51, 1\u201377 (1991)","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"9079_CR5","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1006\/inco.1993.1044","volume":"105","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S., Ong, C.-H.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159\u2013267 (1993)","journal-title":"Inf. Comput."},{"key":"9079_CR6","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90074-C","volume":"91","author":"R. Amadio","year":"1991","unstructured":"Amadio, R.: Recursion over realizability structures. Inf. Comput. 91, 55\u201385 (1991)","journal-title":"Inf. Comput."},{"key":"9079_CR7","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt, H.P., Coppo, M., Dezani, M.: A filter lambda model and the completeness of type assignment. J. Symb. Log. 48, 931\u2013940 (1983)","journal-title":"J. Symb. Log."},{"key":"9079_CR8","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Breazu-Tannen","year":"1991","unstructured":"Breazu-Tannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as implicit coercion. Inf. Comput. 93, 172\u2013221 (1991)","journal-title":"Inf. Comput."},{"key":"9079_CR9","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0890-5401(90)90062-M","volume":"87","author":"K.B. Bruce","year":"1990","unstructured":"Bruce, K.B., Longo, G.: A modest model of records, inheritance and bounded quantification. Inf. Comput. 87, 196\u2013240 (1990)","journal-title":"Inf. Comput."},{"key":"9079_CR10","doi-asserted-by":"crossref","unstructured":"Bruce, K.B., Mitchell, J.C.: Per models of subtyping, recursive types and higher-order polymorphism. In: Proc. of POPL \u201992, pp.\u00a0316\u2013327 (1992)","DOI":"10.1145\/143165.143230"},{"key":"9079_CR11","first-page":"164","volume-title":"Lecture Notes in Computer Science","author":"F. Cardone","year":"1989","unstructured":"Cardone, F.: Relational semantics for recursive types and bounded quantification. In: Lecture Notes in Computer Science, vol.\u00a0372, pp.\u00a0164\u2013178. Springer, Berlin (1989)"},{"key":"9079_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/3-540-45413-6_25","volume-title":"Proc. of TLCA\u201901","author":"U. de\u2019Liguoro","year":"2001","unstructured":"de\u2019Liguoro, U.: Characterizing convergent terms in object calculi via intersection types. In: Proc. of TLCA\u201901. Lecture Notes in Computer Science, vol.\u00a02004, pp.\u00a0315\u2013328. Springer, Berlin (2001)"},{"key":"9079_CR13","series-title":"ENTCS","volume-title":"Proc. of ITRS\u201902","author":"U. de\u2019Liguoro","year":"2002","unstructured":"de\u2019Liguoro, U.: Subtyping in logical form. In: Proc. of ITRS\u201902. ENTCS, vol.\u00a070. Elsevier, Amsterdam (2002)"},{"key":"9079_CR14","doi-asserted-by":"crossref","unstructured":"Gordon, A., Rees, G.: Bisimilarity for first-order calculus of objects with subtyping. In: Proc. of POPL\u201996, pp.\u00a0386\u2013395 (1996)","DOI":"10.1145\/237721.237807"},{"key":"9079_CR15","volume-title":"Lambda-Calcul, Types et Mod\u00e8les","author":"J.L. Krivine","year":"1990","unstructured":"Krivine, J.L.: Lambda-Calcul, Types et Mod\u00e8les. Masson, Paris (1990)"},{"key":"9079_CR16","volume-title":"Foundations for Programming Languages","author":"J.C. Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"key":"9079_CR17","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.tcs.2004.01.030","volume":"316","author":"B. Reus","year":"2004","unstructured":"Reus, B., Streicher, T.: Semantics and logic of object calculi. Theor. Comput. Sci. 316, 191\u2013213 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"9079_CR18","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B.H. Riskov","year":"1994","unstructured":"Riskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"9079_CR19","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. Bakel van","year":"1992","unstructured":"van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput. Sci. 102(1), 135\u2013163 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9079_CR20","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","volume":"151","author":"S. Bakel van","year":"1995","unstructured":"van Bakel, S.: Intersection type assignment systems. Theor. Comput. Sci. 151(2), 385\u2013435 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"9079_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-540-45208-9_17","volume-title":"Proc. of ICTCS\u201903","author":"S. Bakel van","year":"2003","unstructured":"van Bakel, S., de\u2019Liguoro, U.: Logical semantics of the first order sigma-calculus. In: Proc. of ICTCS\u201903. Lecture Notes in Computer Science, vol.\u00a02841, pp.\u00a0202\u2013215. Springer, Berlin (2003)"},{"key":"9079_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/11560586_7","volume-title":"Proc. of ICTCS\u201905","author":"S. Bakel van","year":"2005","unstructured":"van Bakel, S., de\u2019Liguoro, U.: Subtyping object and recursive types logically. In: Proc. of ICTCS\u201905. Lecture Notes in Computer Science, vol.\u00a03701, pp.\u00a066\u201380. Springer, Berlin (2005)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9079-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9079-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9079-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T11:51:35Z","timestamp":1558698695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9079-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,31]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,4]]}},"alternative-id":["9079"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9079-5","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,31]]}}}