2 papers
cs.PL2025
Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact…
cs.PL2025
Baking for Dafny: A CakeML Backend for Dafny
Daniel Nezamabadi, Magnus Myreen
Dafny is a verification-aware programming language that allows developers to formally specify their programs and prove them correct. Currently, a Dafny program is compiled in two s…