Improving the Stability of Type Safety Proofs in Dafny

Explore a method for enhancing the stability of type soundness proofs in Dafny presented in this 20-minute conference talk by Joseph W. Cutler, Michael Hicks, and Emina Torlak at ACM SIGPLAN. Delve into their extended abstract, which introduces a technique for structuring type safety proofs to improve stability. Examine the case study applying this method to a small expression language, and analyze the empirical evidence demonstrating improved resource usage metrics correlated with stability. Discover how this approach can be scaled to realistic proofs, as exemplified by its application in the type soundness proof of the Cedar language.

[Dafny'24] Improving the Stability of Type Safety Proofs in Dafny