{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:49Z","timestamp":1775873569568,"version":"3.50.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2008,9,1]],"date-time":"2008-09-01T00:00:00Z","timestamp":1220227200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2008,9]]},"abstract":"<jats:p>Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean connectives, functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm.<\/jats:p>","DOI":"10.1145\/1391289.1391293","type":"journal-article","created":{"date-parts":[[2008,9,16]],"date-time":"2008-09-16T16:32:40Z","timestamp":1221582760000},"page":"1-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":99,"title":["Semantic subtyping"],"prefix":"10.1145","volume":"55","author":[{"given":"Alain","family":"Frisch","sequence":"first","affiliation":[{"name":"LexiFi, Boulogne-Billancourt, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Castagna","sequence":"additional","affiliation":[{"name":"CNRS, PPS - Universit\u00e9 Paris 7, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V\u00e9ronique","family":"Benzaken","sequence":"additional","affiliation":[{"name":"LRI - Universit\u00e9 Paris Sud, Orsay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,9,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165188"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_4_1","volume-title":"-L","author":"Amadio R.","year":"1998"},{"key":"e_1_2_1_5_1","unstructured":"Asperti A. and Longo G. 1991. Categories Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press Cambridge MA.   Asperti A. and Longo G. 1991. Categories Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press Cambridge MA."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944711"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560586_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.46"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.049"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069793"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","volume":"664","author":"Castagna G."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1033"},{"key":"e_1_2_1_16_1","unstructured":"CDUCE. The Cduce programming language. http:\/\/www.cduce.org.  CDUCE. The Cduce programming language. http:\/\/www.cduce.org."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_19_1","volume-title":"Theoretical Aspects of Computer Software","author":"Damm F. M."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_2_1_21_1","first-page":"1","article-title":"The relevance of semantic subtyping. In Intersection Types and Related Systems","volume":"70","author":"Dezani-Ciancaglini M.","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159829"},{"key":"e_1_2_1_25_1","volume-title":"Semantic Subtyping. In LICS'02","author":"Frisch A."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the ECOOP '03","author":"Gapayev V."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19800261902"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040310"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360209"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/767193.767195"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351242"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.42"},{"key":"e_1_2_1_35_1","volume-title":"Informal Proceedings of the Workshop on Types for Proofs and Programs, H. Geuvers, Ed","author":"Pfenning F.","year":"1993"},{"key":"e_1_2_1_37_1","volume-title":"Elsevier Science Publishers B. V. (North-Holland)","author":"Reynolds J. C."},{"key":"e_1_2_1_38_1","volume-title":"Theoretical Aspects of Computer Software","author":"Reynolds J. C."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.4.527"},{"key":"e_1_2_1_41_1","series-title":"Lecture Notes in Computer Science, vol 789","volume-title":"TACS '94, Proceedings of the Symposium on Theoretical Aspects of Computer Science","author":"Tsuiki H."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111047"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964006"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391289.1391293","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1391289.1391293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:58:04Z","timestamp":1750255084000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391289.1391293"}},"subtitle":["Dealing set-theoretically with function, union, intersection, and negation types"],"short-title":[],"issued":{"date-parts":[[2008,9]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,9]]}},"alternative-id":["10.1145\/1391289.1391293"],"URL":"https:\/\/doi.org\/10.1145\/1391289.1391293","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,9]]},"assertion":[{"value":"2006-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}