Type Qualifier Inference for Java
Java プログラムに対し、新しい型と型間の半順序関係を定義してプログラム中に型を記述すれば後は型推論してくれるシステムの話。型付け規則は given なので、検査したいことをうまく書くことができれば型と関係の定義だけですむので楽。論文では例として、JNI プログラムにおいて Java と C で受け渡される整数を変な使い方をしないか検査するというのと、Javari ベースな不変性解析が挙げられている。もしかすると情報流解析の型システムもこの仕組みに載せられるかも。
author="David Greenfieldboyce and Jeffrey S. Foster",
title="{Type Qualifier Inference for Java}",
booktitle="OOPSLA '07",
publisher="ACM",
pages="321--336",
year="2007"