Proof-Carrying Code, George C. Necula, Peter Lee

を読んだ。内容としては、プログラムの配布者はプログラムを配布する時にそのプログラムの正当性を示した証明を付加し、プログラムを実行する側はその証明を検証することでそのプログラムの安全性を確かめた上で実行できるようになるという話。
やっていることはすでに良く知られている手法を組み合わせているだけという感じなので、今の自分が読むには色々な概念の確認が出来て非常にためになるし興味深い論文だったと思う。
個々のアプリケーションごとにどういった性質を証明したいかということが異なるのでproof ruleをそのアプリケーションごとに決めないといけないのが面倒そうだ。
Logical Frameworkの話あたりが良くわかっていないので調べてみよう。