SLam Calculus

酒井君のところにSLam Calculusのことが書いてあったけど、SLam Calculusは簡単に言えば型付きラムダ計算に、データの機密性のようなものを型として与える計算体系みたいなものかな。確か。
型チェックを通れば機密性の高いデータがそれよりも低いデータから推測されたり部分的に情報を得たりといった情報流が生じることがないということが保証されるって言う話だったと思う。論文は"The SLam Calculus: Programming with Secrecy and Integrity"
でもSLam Calculusでは表現力が不充分だっていう話がLanguage-Based Information-Flow Securityに書いてあったな。
やっぱ結構この論文はサーベイ的な要素が強いから概観を得るのにいいな。