Bonsai: synthesis-based reasoning for type systems

Abstract

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.

Document Details

Document Type
Pub Defense Publication
Publication Date
Dec 27, 2017
Source ID
10.1145/3158150

Entities

People

  • Kartik Chandra
  • Rastislav Bodík

Organizations

  • Defense Advanced Research Projects Agency
  • Google
  • Intel Corporation
  • Mozilla Corporation
  • National Science Foundation
  • Stanford University
  • University of Washington

Tags

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Distributed Systems and Data Platform Development
  • Mathematical Modeling and Probability Theory.