Google, IBM & Meta Certificates — All 10,000+ Courses at 40% Off
One annual plan covers every course and certificate on Coursera. 40% off for a limited time.
Get Full Access
This conference talk presents a research project focused on developing a CakeML backend for Dafny, a verification-aware programming language. Learn how researchers Daniel Nezamabadi and Magnus O. Myreen from Chalmers University of Technology are working to reduce Dafny's trusted computing base (TCB) by creating a new backend that translates Dafny to CakeML, a verified subset of Standard ML. Discover their approach to defining functional big-step semantics for the Dafny intermediate representation to prove correctness of the backend. The 18-minute presentation from the Dafny 2025 workshop (January 19, 2025) explores how this work addresses current limitations in Dafny's compilation process, where neither the backend translation to languages like C# or Rust nor the target language's toolchain are verified.
