Download: PDF, slides (PDF), implementation.
“Pluggable type inference for free” by Martin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed, and Michael D. Ernst. In ASE 2023: Proceedings of the 38th Annual International Conference on Automated Software Engineering, (Luxembourg), Sep. 2023.
A pluggable type system extends a host programming language with type
qualifiers. It lets programmers write types like unsigned
int, secret string, and nonnull object.
Typechecking with pluggable types detects and prevents more errors than
the host type system. However, programmers must write type qualifiers;
this is the biggest obstacle to use of pluggable types in practice. Type
inference can solve this problem. Traditional approaches to type inference
are type-system-specific: for each new pluggable type system, the type
inference algorithm must be extended to build and then solve a system of
constraints corresponding to the rules of the underlying type system.
We propose a novel type inference algorithm that can infer type qualifiers for any pluggable type system with little to no new type-system-specific code — that is, “for free”. The key insight is that extant practical pluggable type systems are flow-sensitive and therefore already implement local type inference. Using this insight, we can derive a global inference algorithm by re-using existing implementations of local inference. Our algorithm runs iteratively in rounds. Each round uses the results of local type inference to produce summaries (specifications) for procedures and fields. These summaries enable improved inference throughout the program in subsequent rounds. The algorithm terminates when the inferred summaries reach a fixed point.
In practice, many pluggable type systems are built on frameworks. By implementing our algorithm once, at the framework level, it can be reused by any typechecker built using that framework. Using that insight, we have implemented our algorithm for the open-source Checker Framework project, which is widely used in industry and on which dozens of specialized pluggable typecheckers have been built. In experiments with 11 distinct pluggable type systems and 12 projects, our algorithm reduced, by 45% on average, the number of warnings that developers must resolve by writing annotations.
Download: PDF, slides (PDF), implementation.
BibTeX entry:
@inproceedings{KelloggDNAE2023,
author = {Martin Kellogg and Daniel Daskiewicz and Loi Ngo Duc Nguyen
and Muyeed Ahmed and Michael D. Ernst},
title = {Pluggable type inference for free},
booktitle = {ASE 2023: Proceedings of the 38th Annual International
Conference on Automated Software Engineering},
address = {Luxembourg},
month = sep,
year = {2023}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.