{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T00:02:19Z","timestamp":1746316939169,"version":"3.28.0"},"reference-count":49,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2003.1210049","type":"proceedings-article","created":{"date-parts":[[2003,12,22]],"date-time":"2003-12-22T17:34:10Z","timestamp":1072114450000},"page":"96-107","source":"Crossref","is-referenced-by-count":9,"title":["Structural subtyping of non-recursive types is decidable"],"prefix":"10.1109","author":[{"given":"V.","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"M.","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"35","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2963"},{"key":"36","first-page":"92","article-title":"U?ber die vollsta?ndigkeit eines gewissen systems der aritmethik ganzer zahlen, in welchem die addition als einzige operation hervortritt","author":"presburger","year":"1929","journal-title":"Comptes Rendus Du Premier Congre?s De Mathe?matiques Des Pays Slaves"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1145\/210184.210187"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40018-9_19"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044481714-3\/50012-6"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371494"},{"key":"43","first-page":"1192","article-title":"Arithmetical classes and types of algebraically closed and real-closed fields","volume":"55","author":"tarski","year":"1949","journal-title":"Bull Amer Math Soc"},{"key":"42","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503292"},{"key":"41","article-title":"Quantifier elimination in term algebras: The case of finite languages","author":"sturm","year":"2002","journal-title":"Computer Algebra in Scientific Computing (CASC)"},{"key":"40","article-title":"Untersuchungen u?ber die axiome des klassenkalku?ls and u?ber \"produktations- und summationsprobleme\", welche gewisse klassen von aussagen betreffen","author":"skolem","year":"1919","journal-title":"Skrifter Utgit av Vidnskapsselskapet i Kristiania I Klasse"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58156-1_26"},{"journal-title":"Introduction to Metamathematics","year":"1952","author":"kleene","key":"23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000657"},{"key":"25","article-title":"On the theory of structural subtyping","volume":"879","author":"kuncak","year":"2003","journal-title":"Technical Report"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5132"},{"key":"28","article-title":"The metamathematics of algebraic systems","volume":"66","author":"mal'cev","year":"1971","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000113"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90209-7"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1139"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.2307\/2267454"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365727"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00033-G"},{"key":"32","first-page":"193","article-title":"The first-order theory of ordering constraints over feature trees","volume":"4","author":"mueller","year":"2001","journal-title":"Discrete Mathematics and Theoretical Computer Science"},{"journal-title":"Program Analysis and Specialization of the C Programming Language","year":"1994","author":"andersen","key":"5"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2878"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1056"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614962"},{"key":"19","first-page":"176","article-title":"Lower bounds on type inference with subtypes","author":"hoand","year":"1995","journal-title":"Proc 22rd ACM POPL"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378855"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614961"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00314-5"},{"key":"13","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","article-title":"The first order properties of products of algebraic systems","volume":"47","author":"feferman","year":"1959","journal-title":"Fundamenta Mathematicae"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","article-title":"The computational complexity of logical theories","volume":"718","author":"ferrante","year":"1979","journal-title":"Lecture Notes in Mathematics"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90080-L"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"journal-title":"Type Inference in Systems of Recursive Types with Subtyping","year":"1999","author":"jim","key":"21"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"49","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000815"},{"key":"48","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00185-2"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185543"},{"key":"44","first-page":"1192","article-title":"Arithmetical classes and types of boolean algebras","volume":"55","author":"tarski","year":"1949","journal-title":"Bull Amer Math Soc"},{"key":"47","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61739-6_52","article-title":"Subtyping constrained types","volume":"1145","author":"trifonov","year":"1996","journal-title":"Lecture Notes in Computer Science"},{"key":"46","first-page":"185","article-title":"Feature trees over arbitrary structures","author":"treinen","year":"1997","journal-title":"Specifying Syntactic Structures"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"}],"event":{"name":"18th Annual IEEE Symposium on Logic in Computer Science","acronym":"LICS-03","location":"Ottawa, Ont., Canada"},"container-title":["18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8592\/27231\/01210049.pdf?arnumber=1210049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,3,31]],"date-time":"2018-03-31T10:08:46Z","timestamp":1522490926000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210049\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":49,"URL":"https:\/\/doi.org\/10.1109\/lics.2003.1210049","relation":{},"subject":[]}}