{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:12:07Z","timestamp":1742955127098,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540875307"},{"type":"electronic","value":"9783540875314"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_32","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"446-460","source":"Crossref","is-referenced-by-count":4,"title":["Syntactic Metatheory of Higher-Order Subtyping"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Dulma","family":"Rodriguez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A.: Implementing a normalizer using sized heterogeneous types. In: McBride, C., Uustalu, T. (eds.) Wksh. on Mathematically Structured Functional Programming, MSFP 2006 (2006)","DOI":"10.14236\/ewic\/MSFP2006.3"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/11753728_39","volume-title":"Computer Science \u2013 Theory and Applications","author":"A. Abel","year":"2006","unstructured":"Abel, A.: Polarized subtyping for sized types. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 381\u2013392. Springer, Heidelberg (2006)"},{"key":"32_CR3","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, Heidelberg (1996)"},{"key":"32_CR4","volume-title":"Domains and Lambda Calculi","author":"R. Amadio","year":"1997","unstructured":"Amadio, R., Curien, P.-L.: Domains and Lambda Calculi. Cambridge University Press, Cambridge (1997)"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Adams, R.: A Modular Hierarchy of Logical Frameworks. Ph.D. thesis, University of Manchester (2005)","DOI":"10.1007\/978-3-540-24849-1_1"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Structural subtyping and the notion of power type. In: Proc. of the 15th ACM Symp. on Principles of Programming Languages, POPL 1988, pp. 70\u201379 (1988)","DOI":"10.1145\/73560.73566"},{"issue":"2","key":"32_CR7","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1016\/S0890-5401(03)00062-2","volume":"184","author":"A.B. Compagnoni","year":"2003","unstructured":"Compagnoni, A.B., Goguen, H.: Typed operational semantics for higher-order subtyping. Inf. Comput.\u00a0184(2), 242\u2013297 (2003)","journal-title":"Inf. Comput."},{"key":"32_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1017\/S0960129505005086","volume":"16","author":"A. Compagnoni","year":"2006","unstructured":"Compagnoni, A., Goguen, H.: Anti-symmetry of higher-order subtyping and equality by subtyping. Math. Struct. in Comput. Sci.\u00a016, 41\u201365 (2006)","journal-title":"Math. Struct. in Comput. Sci."},{"key":"32_CR9","unstructured":"Compagnoni, A., Goguen, H.: Subtyping \u00e0 la Church. In: Barendsen, E., Capretta, V., Geuvers, H., Niqui, M. (eds.) Reflections on Type Theory, \u03bb-calculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud University Nijmegen (2007)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/BFb0022246","volume-title":"Computer Science Logic","author":"A.B. Compagnoni","year":"1995","unstructured":"Compagnoni, A.B.: Decidability of higher-order subtyping with intersection types. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 46\u201360. Springer, Heidelberg (1995)"},{"issue":"4","key":"32_CR11","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys\u00a017(4), 471\u2013522 (1985)","journal-title":"ACM Computing Surveys"},{"key":"32_CR12","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press, Cambridge (1989)"},{"issue":"4\u20135","key":"32_CR13","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1017\/S0956796807006430","volume":"17","author":"R. Harper","year":"2007","unstructured":"Harper, R., Licata, D.: Mechanizing metatheory in a logical framework. J. Func. Program\u00a017(4\u20135), 613\u2013673 (2007)","journal-title":"J. Func. Program"},{"key":"32_CR14","first-page":"173","volume-title":"Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007","author":"D.K. Lee","year":"2007","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: Hofmann, M., Felleisen, M. (eds.) Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007, pp. 173\u2013184. ACM Press, New York (2007)"},{"issue":"1","key":"32_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(76)90009-8","volume":"2","author":"J.-J. L\u00e9vy","year":"1976","unstructured":"L\u00e9vy, J.-J.: An algebraic interpretation of the \u03bb\u03b2K-calculus; and an application of a labelled \u03bb-calculus. Theor. Comput. Sci.\u00a02(1), 97\u2013114 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Toward a typed foundation for method specialization and inheritance. In: Proc. of the 17th ACM Symp. on Principles of Programming Languages, POPL 1990, pp. 109\u2013124 (1990)","DOI":"10.1145\/96709.96719"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Pierce, B.C.: Bounded quantification is undecidable. In: POPL, pp. 305\u2013315 (1992)","DOI":"10.1145\/143165.143228"},{"key":"32_CR18","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"32_CR19","series-title":"Almqvist & Wiksell, Stockholm, 1965","volume-title":"Natural Deduction","author":"D. Prawitz","year":"2006","unstructured":"Prawitz, D.: Natural Deduction. Almqvist & Wiksell, Stockholm, 1965. Republication by Dover Publications Inc., Mineola (2006)"},{"issue":"1,2","key":"32_CR20","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S0304-3975(96)00096-5","volume":"176","author":"B.C. Pierce","year":"1997","unstructured":"Pierce, B.C., Steffen, M.: Higher order subtyping. Theor. Comput. Sci.\u00a0176(1,2), 235\u2013282 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR21","unstructured":"Rodriguez, D.: Algorithmic Subtyping for Higher Order Bounded Quantification. Diploma thesis, LMU Munich (2007)"},{"key":"32_CR22","unstructured":"Steffen, M.: Polarized Higher-Order Subtyping. Ph.D. thesis, Technische Fakult\u00e4t, Universit\u00e4t Erlangen (1998)"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgements and properties. Tech. rep., School of Computer Science. Carnegie Mellon University, Pittsburgh (2003)","DOI":"10.21236\/ADA418517"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:14:27Z","timestamp":1715058867000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}