{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T17:25:48Z","timestamp":1672248348527},"reference-count":11,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4933,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,9]]},"abstract":"<jats:p>We study a type system with a notion of subtyping that involves a largest type \u22a4, a smallest type \u22a5, atomic coercions between base types, and the usual ordering of function types. We prove that any \u03bb-term typable in this system is strongly normalizing, which solves an open problem of Thatte. We also prove that the fragment without \u22a5 types has strictly fewer terms. This demonstrates that \u22a5 adds power to a type system.<\/jats:p>","DOI":"10.1017\/s0960129500000815","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:13Z","timestamp":1236157273000},"page":"419-429","source":"Crossref","is-referenced-by-count":4,"title":["Strong normalization with non-structural subtyping"],"prefix":"10.1017","volume":"5","author":[{"given":"Mitchell","family":"Wand","sequence":"first","affiliation":[]},{"given":"Patrick","family":"O'Keefe","sequence":"additional","affiliation":[]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000815_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19488-6_146"},{"key":"S0960129500000815_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90196-3"},{"key":"S0960129500000815_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80051-0"},{"key":"S0960129500000815_ref001","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S0960129500000815_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_24"},{"key":"S0960129500000815_ref008","unstructured":"R\u00e9my D. (1989) Typechecking records and variants in a natural extension of ML. Sixteenth Symposium on Principles of Programming Languages 77\u201388."},{"key":"S0960129500000815_ref002","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5101"},{"key":"S0960129500000815_ref003","doi-asserted-by":"crossref","unstructured":"Gomard C. K. (1990) Partial type inference for untyped functional programs. Proc. ACM Conference on Lisp and Functional Programming 282\u2013287.","DOI":"10.1145\/91556.91672"},{"key":"S0960129500000815_ref005","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000113"},{"key":"S0960129500000815_ref010","doi-asserted-by":"publisher","DOI":"10.1145\/502949.502895"},{"key":"S0960129500000815_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90050-C"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000815","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T21:03:27Z","timestamp":1557781407000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000815\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["S0960129500000815"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000815","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}