A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. - Torben Amtoft; Josiah Dodds; Zhi Zhang; Andrew W. Appel; Lennart Beringer; John Hatcliff; Xinming Ou; Andrew Cousino (POST, 2012)