Bonsai: synthesis-based reasoning for type systems

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 s...