{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:17Z","timestamp":1725496817041},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_30","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"420-438","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Anti-Symmetry of Higher-Order Subtyping"],"prefix":"10.1007","author":[{"given":"Adriana","family":"Compagnoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Healfdene","family":"Goguen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.","DOI":"10.1007\/978-1-4419-8598-9"},{"issue":"4","key":"30_CR2","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R. M. Amadio","year":"1993","unstructured":"R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575\u2013631, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"30_CR3","unstructured":"D. Aspinall and A. Compagnoni. Subtyping dependent types. In Eleventh Annual IEEE Symposium on Logic in Computer Science,New Brunswick,New Jersey, USA, July 1996. Long version to appear in Theoretical Computer Science."},{"issue":"4","key":"30_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. Afilter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931\u2013940, 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"30_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172\u2013221, 1991.","journal-title":"Information and Computation"},{"key":"30_CR6","unstructured":"K. B. Bruce. Typing in object-oriented languages: Achieving expressiveness and safety. Unpublished, June 1996."},{"key":"30_CR7","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1016\/0890-5401(90)90062-M","volume":"87","author":"K. B. Bruce","year":"1990","unstructured":"K. B. Bruce and G. Longo. Amo dest model of records, inheritance, and bounded quantification. Information and Computation, 87:196\u2013240, 1990.","journal-title":"Information and Computation"},{"key":"30_CR8","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1016\/0890-5401(88)90007-7","volume":"76","author":"L. Cardelli","year":"1988","unstructured":"L. Cardelli. Aseman tics of multiple inheritance. Information and Computation, 76:138\u2013164, 1988.","journal-title":"Information and Computation"},{"key":"30_CR9","unstructured":"L. Cardelli. Notes about F\n\n<\n\u2264\n. Unpublished manuscript, Oct. 199"},{"issue":"4","key":"30_CR10","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1017\/S0956796800000198","volume":"1","author":"L. Cardelli","year":"1991","unstructured":"L. Cardelli and G. Longo. Aseman tic basis for Quest. Journal of Functional Programming, 1(4):417\u2013458, Oct. 1991.","journal-title":"Journal of Functional Programming"},{"key":"30_CR11","series-title":"Lect Notes Comput Sci","first-page":"3","volume-title":"Mathematical Structures in Computer Science","author":"L. Cardelli","year":"1991","unstructured":"L. Cardelli and J. Mitchell. Operations on records. Mathematical Structures in Computer Science, 1:3\u201348, 1991. Also in [23], and available as DEC Systems Research Center Research Report #48, August, 1989, and in the proceedings of MFPS\u2019 89, Springer LNCS volume 442."},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), Dec. 1985.","DOI":"10.1145\/6041.6042"},{"key":"30_CR13","unstructured":"J. Chroboczek. Game Semantics and Subtyping. PhD thesis, University of Edinburgh, 1999. Forthcoming Thesis. Supervisor: Prof. S. Abramsky."},{"key":"30_CR14","unstructured":"A. Compagnoni and H. Goguen. Decidability of higher-order subtyping via logical relations, Dec. 1997."},{"key":"30_CR15","unstructured":"A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. Submitted to Information and Computation."},{"key":"30_CR16","series-title":"PhD thesis","volume-title":"Higher-Order Subtyping with Intersection Types","author":"A. B. Compagnoni","year":"1995","unstructured":"A. B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, The Netherlands, Jan. 1995. Supervisor: Prof. Barendregt. ISBN 90-9007860-6."},{"key":"30_CR17","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1017\/S0960129500070043","volume":"6","author":"A. B. Compagnoni","year":"1996","unstructured":"A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6:469\u2013501, 1996.","journal-title":"Mathematical Structures in Computer Science"},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF02011875","volume":"19","author":"M. Coppo","year":"1978","unstructured":"M. Coppo and M. Dezani-Ciancaglini. Anew type-assignment for \u03bb-terms. Archiv. Math. Logik, 19:139\u2013156, 1978.","journal-title":"Archiv. Math. Logik"},{"key":"30_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1007\/3-540-54415-1_72","volume-title":"Theoretical Aspects of Computer Software (Sendai,Jap an)","author":"P.-L. Curien","year":"1991","unstructured":"P.-L. Curien and G. Ghelli. Subtyping + extensionality: Confluence of \u00df?-reductions in F=. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai,Jap an), number 526 in Lecture Notes in Computer Science, pages 731\u2013749._Springer-Verlag, Sept. 1991."},{"key":"30_CR20","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1017\/S0960129500001134","volume":"2","author":"P.-L. Curien","year":"1992","unstructured":"P.-L. Curien and G. Ghelli. Coherence of subsumption: Minimum typing and typechecking in F=. Mathematical Structures in Computer Science, 2:55\u201391, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"30_CR21","unstructured":"D. Duggan and A. Compagnoni. Subtyping for object type constructors. In Foundations of Object-Oriented Languages (FOOL 6). http:\/\/www.cs.williams.edu\/ ~kim\/FOOL\/sched6.html, 1999."},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"H. Goguen. Typed operational semantics. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 186\u2013200. Springer-Verlag, Apr. 1995.","DOI":"10.1007\/BFb0014053"},{"key":"30_CR23","unstructured":"C. A. Gunter and J. C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types,Semantics,and Language Design. The MIT Press, 1994."},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"M. Hofmann and B. Pierce. Positive subtyping. Information and Computation, 126(1), 1996.","DOI":"10.1006\/inco.1996.0031"},{"key":"30_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TYPES\u201996","author":"A. Jones","year":"1996","unstructured":"A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. In Proceedings of TYPES\u201996, Lecture Notes in Computer Science, 1996."},{"key":"30_CR26","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"30_CR27","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109\u2013124, Jan. 1990.","DOI":"10.1145\/96709.96719"},{"key":"30_CR28","unstructured":"J. C. Mitchell, F. Honsell, and K. Fisher. Alam bda calculus of objects and method specialization. In 1993 IEEE Symposium on Logic in Computer Science, June 1993."},{"key":"30_CR29","unstructured":"F. Pfenning. Refinement types for logical frameworks. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pages 315\u2013328, May 1993."},{"issue":"1-2","key":"30_CR30","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S0304-3975(96)00096-5","volume":"176","author":"B. Pierce","year":"1997","unstructured":"B. Pierce and M. Steffen. Higher-order subtyping. Theoretical Computer Science, 176(1-2):235\u2013282, 1997. corrigendum in TCS vol. 184 (1997), p. 247.","journal-title":"Theoretical Computer Science"},{"key":"30_CR31","doi-asserted-by":"crossref","unstructured":"B. C. Pierce. Bounded quantification is undecidable. Information and Computation, 1993.","DOI":"10.1145\/143165.143228"},{"key":"30_CR32","volume-title":"Technical Report 492","author":"B. C. Pierce","year":"1997","unstructured":"B. C. Pierce. Bounded quantification with bottom. Technical Report 492, Computer Science Department, Indiana University, 1997."},{"key":"30_CR33","unstructured":"M. Steffen. Polarized Higher-Order Subtyping. PhD thesis, Lehrstuhl f\u00fcr Informatik VII, Friedrich Alexander Universit\u00e4t Erlangen-N\u00fcrnberg, 1998."},{"key":"30_CR34","doi-asserted-by":"crossref","unstructured":"J. Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. In Proceedings of FST-TCS\u201995, 1995.","DOI":"10.1007\/3-540-60692-0_47"},{"key":"30_CR35","unstructured":"J. Zwanenburg. An Object Oriented Programming Logic Based on Type Theory. PhD thesis, Eindhoven University of Technology, 1999. Supervisor: Prof. Hemerik."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T04:09:31Z","timestamp":1586146171000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}