Josiah Dodds, Andrew W. Appel: Mostly Sound Type System Improves a Foundational Program Verifier. CPP 2013: 17-32