In this extended abstract, we present a method for structuring type soundness proofs in Dafny to improve proof stability. As a case study, we apply the method to proving type soundness for a small expression language, and demonstrate empirically how it improves resource usage metrics known to correlate with stability. Our method can scale to realistic proofs, as demonstrated by its use in the type soundness proof of the Cedar language.

[ .pdf ]

@misc{cutler24typesafety,
  author = {Joseph W. Cutler and Michael Hicks and Emina Torlak},
  title = {Improving the Stability of Type Safety Proofs in {Dafny}},
  note = {Dafny Workshop talk},
  year = 2024,
  month = jan
}

This file was generated by bibtex2html 1.99.