{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T05:29:36Z","timestamp":1736573376475,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540648277"},{"type":"electronic","value":"9783540685326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055782","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T17:36:31Z","timestamp":1155836191000},"page":"326-335","source":"Crossref","is-referenced-by-count":0,"title":["Predicative polymorphic subtyping"],"prefix":"10.1007","author":[{"given":"Marcin","family":"Benke","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,28]]},"reference":[{"key":"29_CR1","unstructured":"Marcin Benke. Predicative polymorphic subtyping. Technical Report TR98-02(251), Institute of Informatics, Warsaw University, March 1998. Available from http:\/\/zls.mimuw.edu.pl\/~ben\/Papers\/."},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Jacek Chrzaszcz. Polimorphic subtyping without distributivity. MFCS'98 (in this volume), 1998.","DOI":"10.1007\/BFb0055784"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 207\u2013211, 1982.","DOI":"10.1145\/582153.582176"},{"key":"29_CR4","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithmetique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"29_CR5","unstructured":"Trevor Jim. System F plus subsumption reduces to Mitchell's subtyping relation. Manuscript, 1995."},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Trevor Jim. What are principal typings and what are they good for? In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 42\u201353, 1996.","DOI":"10.1145\/237721.237728"},{"issue":"98","key":"29_CR7","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/0890-5401(92)90020-G","volume":"2","author":"A. J. Kfoury","year":"1992","unstructured":"A. J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments of the second-order \u03bb-calculus. Information and Computation, 2(98):228\u2013257, June 1992.","journal-title":"Information and Computation"},{"key":"29_CR8","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0890-5401(91)90053-5","volume":"93","author":"D. Leivant","year":"1991","unstructured":"Daniel Leivant. Finitely stratified polymorphism. Information and Computation, 93:93\u2013113, 1991.","journal-title":"Information and Computation"},{"key":"29_CR9","unstructured":"G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping. In Proc. IEEE Symp. on Logic in Computer Science, pages 292\u2013299, 1995."},{"issue":"5","key":"29_CR10","doi-asserted-by":"publisher","first-page":"1411","DOI":"10.1145\/186025.186031","volume":"16","author":"K. L\u00e4ufer","year":"1994","unstructured":"Konstantin L\u00e4ufer and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411\u20131430, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"14","key":"29_CR11","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(14):348\u2013375, December 1978.","journal-title":"Journal of Computer and System Sciences"},{"issue":"2\/3","key":"29_CR12","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"J. C. Mitchell","year":"1988","unstructured":"John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2\/3):211\u2013249, 1988. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 153\u2013194.","journal-title":"Information and Computation"},{"issue":"3","key":"29_CR13","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J. Mitchell","year":"1988","unstructured":"John Mitchell and Gordon Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3):470\u2013502, 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Martin Odersky and Konstantin L\u00e4ufer. Putting type annotations to work. In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 54\u201367, 1996.","DOI":"10.1145\/237721.237729"},{"key":"29_CR15","unstructured":"N. Perry. The Implementation of Practical Functional Programming Languages. PhD thesis, Imperial College of Science, Technology, and Medicine, University of London, 1990."},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Didier R\u00e9my. Programming objects with ml-art, and extension to ml with abstract and record types. In Proceedings of Theoretical Aspects of Programming Languages, number 789 in LNCS, pages 321\u2013346. Springer, 1994.","DOI":"10.1007\/3-540-57887-0_102"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Mathematical foundations of software development. volume 19 of Lecture Notes in Computer Science, chapter Towards a theory of type structure., pages 408\u2013425. Springer, 1974.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Jerzy Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. In Ed. P.S. Thiagarajan, editor, Proc. 15th Conference Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 166\u2013179. Springer Verlag, 1995.","DOI":"10.1007\/3-540-60692-0_47"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types is undecidable. In Proceedings of 11th LICS, 1996.","DOI":"10.1109\/LICS.1996.561306"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"J. Wells. Typability and type checking in the second-order \u03bb-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Symp. Logic in Comput. Sci., pages 176\u2013185, 1994.","DOI":"10.1109\/LICS.1994.316068"},{"key":"29_CR21","unstructured":"J. Wells. The undecidability of Mitchell's subtyping relation. Technical report, Computer Sci. Dept., Boston University, December 1995."},{"key":"29_CR22","unstructured":"J. B. Wells. Typability is undecidable for F+eta. Technical Report 96-022, Boston University, March 9, 1996."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1998"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T13:52:45Z","timestamp":1736517165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055782"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540648277","9783540685326"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0055782","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}