Effective interactive proofs for higher-order imperative programs.

Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

Browse the full ICFP paper archive.