State of the Union: Type Inference via Craig Interpolation

State of the Union: Type Inference via Craig Interpolation, by Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu

The ad-hoc use of unions to encode disjoint sum types in C programs and the inability of C's type system to check the safe use of these unions is a long standing source of subtle bugs. We present a dependent type system that rigorously captures the ad-hoc protocols that programmers use to encode disjoint sums, and introduce a novel technique for automatically inferring, via Craig Interpolation, those dependent types and thus those protocols. In addition to checking the safe use of unions, the dependent type information inferred by interpolation gives programmers looking to modify or extend legacy code a precise understanding of the conditions under which some fields may be safely accessed. We present an empirical evaluation of our technique on 350KLOC of open source C code. In 80 out of 90 predicated edges (corresponding to 1472 out of 1684 union accesses), our type system is able to infer the correct dependent types. This demonstrates that our type system captures and explicates programmers' informal reasoning about unions, without requiring manual annotation or rewriting.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

That's neat -- I had never

That's neat -- I had never heard of Craig interpolation before.

Very nice

I knew of hardly any of the work in this area: good call. Their occassional collaborator Ken McMillar seems to have cleared the grounds for this work: his Applications of Craig Interpolants in Model Checking seems especially interesting[*], as are some other of his papers.

[*] The basic idea of the paper is that the interpolation property can save you a lot of expensive quantifier elimination when doing model checking.

Implementation of Craig Interpolation?

Unfortunately, it looks like the implementation of Craig Interpolation that they're working with is copyright Cadence Systems, and they can't release the source. Anybody know of another implementation? I would love to see how it's done.

Standard proof theory

There are many techniques for doing this, but usually the easiest to understand is by deriving it as a corollary to cut-elimination. A caveat: the fit between cut-freeness and interpolation isn't exact: there are logics for which it is easier to show interpolation than try to come up with a cut-free characterisation, and there are cut-free characterisations of logics which don't have interpolation.