{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:44Z","timestamp":1779836744585,"version":"3.53.1"},"reference-count":86,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T00:00:00Z","timestamp":1330992000000},"content-version":"unspecified","delay-in-days":65,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on a Satisfiability Modulo Theories solver to compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows us to show the uniqueness of normal forms for non-deterministic expressions, provide precise counterexamples when type-checking fails, detect empty types, and compute instances of types statically and at run-time.<\/jats:p>","DOI":"10.1017\/s0956796812000032","type":"journal-article","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T08:18:06Z","timestamp":1331021886000},"page":"31-105","source":"Crossref","is-referenced-by-count":16,"title":["Semantic subtyping with an SMT solver"],"prefix":"10.1017","volume":"22","author":[{"given":"GAVIN M.","family":"BIERMAN","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREW D.","family":"GORDON","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u0102T\u0102LIN","family":"HRI\u0162CU","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DAVID","family":"LANGWORTHY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,3,6]]},"reference":[{"key":"S0956796812000032_ref81","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming","author":"Tobin-Hochstadt","year":"2010"},{"key":"S0956796812000032_ref78","volume-title":"Proceedings of ESOP","author":"Swamy","year":"2010"},{"key":"S0956796812000032_ref76","volume-title":"Proceedings of POPL","author":"Sim\u00e9on","year":"2003"},{"key":"S0956796812000032_ref68","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796812000032_ref69","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"S0956796812000032_ref72","first-page":"173","volume-title":"Algol-Like Languages","author":"Reynolds","year":"1996"},{"key":"S0956796812000032_ref74","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"S0956796812000032_ref84","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"S0956796812000032_ref55","volume-title":"Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Komondoor","year":"2005"},{"key":"S0956796812000032_ref60","volume-title":"Proceedings of LFMTP","author":"Lovas","year":"2007"},{"key":"S0956796812000032_ref9","volume-title":"Proceedings of CAV","author":"Barrett","year":"2007"},{"key":"S0956796812000032_ref50","volume-title":"Systematic Software Development Using VDM","author":"Jones","year":"1986"},{"key":"S0956796812000032_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00024-Q"},{"key":"S0956796812000032_ref66","volume-title":"Proceedings of IFIP","author":"Nordstr\u00f6m","year":"1983"},{"key":"S0956796812000032_ref46","volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming","author":"Hosoya","year":"2000"},{"key":"S0956796812000032_ref20","volume-title":"Proceedings of LISP Conference","author":"Burstall","year":"1980"},{"key":"S0956796812000032_ref24","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3128"},{"key":"S0956796812000032_ref75","volume-title":"Proceedings of OOPSLA","author":"Saraswat","year":"2008"},{"key":"S0956796812000032_ref3","volume-title":"Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Aiken","year":"1994"},{"key":"S0956796812000032_ref15","volume-title":"Proceedings of TPHOLs","author":"B\u00f6hme","year":"2008"},{"key":"S0956796812000032_ref11","volume-title":"Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Benzaken","year":"2003"},{"key":"S0956796812000032_ref58","volume-title":"Proceedings of the ACM Symposium on Applied Computing","author":"Leino","year":"2009"},{"key":"S0956796812000032_ref28","first-page":"183","volume-title":"Proceedings of CADE-21","author":"de Moura","year":"2007"},{"key":"S0956796812000032_ref49","volume-title":"Proceedings of TACAS","author":"Jhala","year":"2007"},{"key":"S0956796812000032_ref13","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Bierman","year":"2010"},{"key":"S0956796812000032_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"S0956796812000032_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/767193.767195"},{"key":"S0956796812000032_ref65","volume-title":"The Microsoft Code Name \u201cM\u201d Modeling Language Specification Version 0.5","year":"2009"},{"key":"S0956796812000032_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"S0956796812000032_ref77","volume-title":"Proceedings of TYPES","author":"Sozeau","year":"2006"},{"key":"S0956796812000032_ref53","volume-title":"Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types and Dynamic","author":"Knowles","year":"2007"},{"key":"S0956796812000032_ref29","volume-title":"Proceedings of TACAS","author":"de Moura","year":"2008"},{"key":"S0956796812000032_ref27","volume-title":"Proceedings of TACS","author":"Damm","year":"1994"},{"key":"S0956796812000032_ref30","volume-title":"Proceedings of FMCAD","author":"de Moura","year":"2009"},{"key":"S0956796812000032_ref4","volume-title":"Proceedings of CSL","author":"Aspinall","year":"1994"},{"key":"S0956796812000032_ref38","volume-title":"Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation","author":"Freeman","year":"1991"},{"key":"S0956796812000032_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"S0956796812000032_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9085-y"},{"key":"S0956796812000032_ref16","unstructured":"Box D. (2010) Update on SQL Server Modeling CTP (Repository\/Modeling Services, \u201cQuadrant\u201d and \u201cM\u201d). Accessed September 22, 2010. Blog available at http:\/\/blogs.msdn.com\/b\/modelcitizen"},{"key":"S0956796812000032_ref42","volume-title":"Proceedings of ISSS","author":"Gordon","year":"2002"},{"key":"S0956796812000032_ref1","volume-title":"Data on the Web","author":"Abiteboul","year":"2000"},{"key":"S0956796812000032_ref82","unstructured":"TypiCal Project 2009 The Coq Proof Assistant. Version 8.2. Accessed February 27, 2012. Available at: http:\/\/coq.inria.fr."},{"key":"S0956796812000032_ref5","volume-title":"Advanced Topics in Types and Programming Languages","author":"Aspinall","year":"2005"},{"key":"S0956796812000032_ref36","volume-title":"Proceedings of the Symposium on Principles of Programming Languages","author":"Fisher","year":"2006"},{"key":"S0956796812000032_ref2","volume-title":"Proceedings of ICFP 03, the Eighth ACM SIGPLAN International Conference on Functional Programming","author":"Aiken","year":"1993"},{"key":"S0956796812000032_ref10","volume-title":"Proceedings of CSF","author":"Bengtson","year":"2008"},{"key":"S0956796812000032_ref25","volume-title":"Proceedings of SIGMOD","author":"Cohen","year":"2006"},{"key":"S0956796812000032_ref8","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213008004060"},{"key":"S0956796812000032_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"S0956796812000032_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(94)00215-7"},{"key":"S0956796812000032_ref86","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Xi","year":"1999"},{"key":"S0956796812000032_ref6","volume-title":"Proceedings of CPP, the 11th Generative Approaches to Second Language Acquisition Conference","author":"Backes","year":"2011"},{"key":"S0956796812000032_ref70","volume-title":"Proceedings of POPL","author":"Pratt","year":"1983"},{"key":"S0956796812000032_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"S0956796812000032_ref26","doi-asserted-by":"publisher","DOI":"10.17487\/rfc4627"},{"key":"S0956796812000032_ref40","volume-title":"Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation","author":"Genev\u00e8s","year":"2007"},{"key":"S0956796812000032_ref64","volume-title":"Eiffel: The Language","author":"Meyer","year":"1992"},{"key":"S0956796812000032_ref56","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science","author":"Kopylov","year":"2003"},{"key":"S0956796812000032_ref22","volume-title":"Proceedings of PLDI","author":"Cartwright","year":"1991"},{"key":"S0956796812000032_ref23","volume-title":"Proceedings of DBPL","author":"Castagna","year":"2005"},{"key":"S0956796812000032_ref35","volume-title":"Proceedings of the SeventhACM SIGPLAN International Conference on Functional Programming (ICFP '02)","author":"Findler","year":"2002"},{"key":"S0956796812000032_ref80","volume-title":"Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Tobin-Hochstadt","year":"2008"},{"key":"S0956796812000032_ref59","volume-title":"Proceedings of PLDI","author":"Lerner","year":"2007"},{"key":"S0956796812000032_ref7","volume-title":"Proceedings of FMCO","author":"Barnett","year":"2005"},{"key":"S0956796812000032_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"S0956796812000032_ref48","first-page":"470","volume-title":"Proceedings of CAV","author":"Jhala","year":"2011"},{"key":"S0956796812000032_ref33","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL","author":"Dunfield","year":"2004"},{"key":"S0956796812000032_ref83","volume-title":"Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming","author":"Unno","year":"2009"},{"key":"S0956796812000032_ref62","volume-title":"Proceedings of SIGMOD","author":"Meijer","year":"2007"},{"key":"S0956796812000032_ref41","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005797629953"},{"key":"S0956796812000032_ref71","volume-title":"The SMT-LIB Standard: Version 1.2","author":"Ranise","year":"2006"},{"key":"S0956796812000032_ref43","volume-title":"Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Greenberg","year":"2010"},{"key":"S0956796812000032_ref37","volume-title":"Proceedings of the Symposium on Principles of Programming Languages","author":"Flanagan","year":"2006"},{"key":"S0956796812000032_ref14","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (OOPSLA)","author":"Bierman","year":"2007"},{"key":"S0956796812000032_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"S0956796812000032_ref32","unstructured":"Dunfield J. (Aug. 2007) A Unified System of Type Refinements. PhD. thesis, CMU-CS-07-129, Carnegie Mellon University, Pittsburgh, PA."},{"key":"S0956796812000032_ref34","unstructured":"Dutertre B. & de Moura L. M. . The YICES SMT solver. Accessed February 27, 2012. Available at: http:\/\/yices.csl.sri.com\/tool-paper.pdf, 2006."},{"key":"S0956796812000032_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005404"},{"key":"S0956796812000032_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"S0956796812000032_ref44","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006338"},{"key":"S0956796812000032_ref61","volume-title":"Proceedings of IFIP Congress","author":"McCarthy","year":"1962"},{"key":"S0956796812000032_ref79","volume-title":"Proceedings of POPL","author":"Terauchi","year":"2010"},{"key":"S0956796812000032_ref19","volume-title":"Proceedings of DBPL","author":"Buneman","year":"1999"},{"key":"S0956796812000032_ref85","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796812000032_ref73","volume-title":"Proceedings of PLDI","author":"Rondon","year":"2008"},{"key":"S0956796812000032_ref67","volume-title":"Programming with Intersection Types, Union Types, and Polymorphism","author":"Pierce","year":"1991"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:25Z","timestamp":1779834985000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000032\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":86,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["S0956796812000032"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000032","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1]]}}}