Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems
並行プログラムを対象とする情報流解析の型システムが非干渉性に対して健全であることを Isabelle/HOL を使って示したという論文。逐次プログラムの非干渉性は、高機密度のデータのみが異なる初期状態から実行した結果が区別できないことだけど、並行プログラムの場合は利アクティブ性を考慮して bisimilarity を要求する。それと、スケジューリングの方法によって実行が変わるのでスケジューラを考慮できるようにする。というセッティングのもとで健全性を証明。
author="Gilles Barthe and Leonor Prensa Nieto",
title="{Formally Verifying Information Flow Type Systems for Cuncurrent and Thread Systems}",
booktitle="FMSE '04",
publisher="ACM",
pages="13--22",
year="2004"