{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:50Z","timestamp":1750221290235,"version":"3.41.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Intel","award":["gift"],"award-info":[{"award-number":["gift"]}]},{"name":"Mozilla","award":["gift"],"award-info":[{"award-number":["gift"]}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA8750--16--2--0032"],"award-info":[{"award-number":["FA8750--16--2--0032"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["gift"],"award-info":[{"award-number":["gift"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF--1139138,CCF--1337415,ACI--1535191"],"award-info":[{"award-number":["CCF--1139138,CCF--1337415,ACI--1535191"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>When designing a type system, we may want to mechanically check the design to guide its further development. We describe algorithms that perform symbolic reasoning about executable models of type systems. The algorithms support three queries. First, they check type soundness and synthesize a counterexample program if such a soundness bug is found. Second, they compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, they minimize the size of synthesized counterexample programs.<\/jats:p>\n          <jats:p>\n            These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of the various possible input programs. Our main contribution is the\n            <jats:italic>bonsai tree<\/jats:italic>\n            , a novel symbolic representation of programs and program states that addresses these challenges. Bonsai trees encode complex syntactic information in terms of logical constraints, enabling more efficient merging.\n          <\/jats:p>\n          <jats:p>We implement these algorithms in the Bonsai tool, an assistant for type system designers. We perform case studies on how Bonsai helps test and explore a variety of type systems. Bonsai efficiently synthesizes counterexamples for soundness bugs previously inaccessible to automatic tools and is the first automated tool to find a counterexample for the recently discovered Scala soundness bug SI-9633.<\/jats:p>","DOI":"10.1145\/3158150","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Bonsai: synthesis-based reasoning for type systems"],"prefix":"10.1145","volume":"2","author":[{"given":"Kartik","family":"Chandra","sequence":"first","affiliation":[{"name":"Henry M. Gunn High School, USA \/ Stanford University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984004"},{"volume-title":"Soundness issue with path-dependent type on \u2018null\u2018 path. https:\/\/issues.scala-lang.org\/browse\/SI-9633","year":"2016","author":"Amin Nada","key":"e_1_2_2_3_1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"volume-title":"MIT Laboratory for Computer Science","year":"2003","author":"Andoni Alexandr","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/356914.356918"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.2"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604156"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(85)90004-4"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.4.305"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642963"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.65"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053388"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004562"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.840301"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831712"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567454"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320395"},{"key":"e_1_2_2_31_1","unstructured":"JPF. JavaPathFinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/ .  JPF. JavaPathFinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/ ."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103691"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103691"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-013-9091-1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_2_2_37_1","unstructured":"Daniel Kroening. CBMC. http:\/\/www.cprover.org\/cbmc\/ .  Daniel Kroening. CBMC. http:\/\/www.cprover.org\/cbmc\/ ."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/335231.335240"},{"volume-title":"Higher-order symbolic execution for contract verification and refutation. CoRR, abs\/1507.04817","year":"2015","author":"Nguyen Phuc C.","key":"e_1_2_2_40_1"},{"first-page":"170","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"Nipkow Tobias","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_2_43_1","unstructured":"Martin Odersky. We got liftoff! The Dotty compiler for Scala bootstraps. http:\/\/www.scala-lang.org\/blog\/2015\/10\/23\/dotty-compiler-bootstraps.html 2015.  Martin Odersky. We got liftoff! The Dotty compiler for Scala bootstraps. http:\/\/www.scala-lang.org\/blog\/2015\/10\/23\/dotty-compiler-bootstraps.html 2015."},{"key":"e_1_2_2_44_1","unstructured":"Martin Odersky. Scaling DOT to Scala - soundness. http:\/\/scala-lang.org\/blog\/2016\/02\/17\/scaling-dot-soundness.html 2016.  Martin Odersky. Scaling DOT to Scala - soundness. http:\/\/scala-lang.org\/blog\/2016\/02\/17\/scaling-dot-soundness.html 2016."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.840306"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869461"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449803"},{"volume-title":"Casey Klein and Matthias Felleisen","year":"2017","author":"Robert Bruce Findler Burke Fetscher","key":"e_1_2_2_50_1"},{"volume-title":"Purdue University and EPFL","year":"2016","author":"Rompf Tiark","key":"e_1_2_2_51_1"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951915"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491447"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_31"},{"volume-title":"The Coq proof assistant reference manual. LogiCal Project","year":"2004","author":"The Coq","key":"e_1_2_2_59_1"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"volume-title":"The Rosette Guide","year":"2016","author":"Torlak Emina","key":"e_1_2_2_62_1"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134022"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48166-4_16"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158150","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158150","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158150","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158150"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":64,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158150"],"URL":"https:\/\/doi.org\/10.1145\/3158150","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}