上の論文は C の共用体の型推論を Craig Interpolation によって行う試みについて述べています。
この試みには次のような背景があります; 共用体の一般的な使い道として、異なる型の直和を渡る変数のコーディングがあります。しかし、コンパイラがプログラム中でその変数が安全に使われているかどうかをチェックしていない場合、誤った型にキャストされる可能性があります。K&R ではこの点について次のように述べています(6.8節):
どの型がいま共用体に格納されているかを覚えておくのは、プログラマの責任である。あるデータがある型として格納され、しかもそれ以外の型として取り出されたときは、結果は処理系に依存するものとなる。
実行時にインスタンスがどの型を持っているかを判断しなければなりません。そのための典型的なテクニックとして、型の情報を持つタグフィールドがあります。例として ICMP のヘッダが挙げられています。上の論文ではこの手法を形式化する型システムを定義し、共用体の状態を制約として記述する論理で interpolants をとることで安全性をチェックしようとしています。
この中心となるアイディアは馴染みやすく、また実装に用いている CIL というライブラリも有用そうだと思いました。