Bonsai - Synthesis-Based Reasoning for Type Systems

Watch a 25-minute conference talk from POPL 2018 exploring Bonsai, a groundbreaking tool for automated reasoning about type systems. Learn how Bonsai uses symbolic evaluation and a novel tree representation to help type system designers test and validate their work through three key capabilities: checking type soundness with counterexample synthesis, comparing different versions of type systems, and minimizing counterexample programs. Discover how this innovative approach successfully uncovered previously inaccessible soundness bugs, including the notable Scala SI-9633 bug, through efficient handling of complex syntactic information using logical constraints. Presented by Kartik Chandra from Stanford University and Rastislav Bodik from the University of Washington, this talk demonstrates practical applications in type checking, synthesis, and symbolic compilation.