标题： 为Dafny烘焙：Dafny的CakeML后端 显示英文标题

标题： Baking for Dafny: A CakeML Backend for Dafny

摘要： Dafny是一种注重验证的编程语言，允许开发人员正式指定他们的程序并证明其正确性。 目前，Dafny程序通过两个步骤进行编译：首先，后端将输入程序转换为像C#或Rust这样的高级目标语言。 其次，转换后的程序使用目标语言的工具链进行编译。 最近，Dafny添加了一个中间表示（IR），作为新后端的输入。 在撰写本文时，这些步骤均未经过验证，导致后端和目标语言的工具链都成为Dafny的信任计算基础（TCB）的一部分。 为了减少Dafny的TCB，我们开始开发一个新后端，该后端将Dafny翻译为CakeML，这是一种经过验证的、自举的Standard ML子集，在交互式定理证明器HOL4中实现。 我们还开始为Dafny IR定义功能性的大步语义，以证明后端的正确性。 显示英文摘要

摘要： 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 steps: First, a backend translates the input program to a high-level target language like C# or Rust. Second, the translated program is compiled using the target language's toolchain. Recently, an intermediate representation (IR) has been added to Dafny that serves as input to new backends. At the time of writing, none of these steps are verified, resulting in both the backend and the target language's toolchain being part of Dafny's trusted computing base (TCB). To reduce Dafny's TCB, we started developing a new backend that translates Dafny to CakeML, a verified, bootstrapped subset of Standard ML, in the interactive theorem prover HOL4. We also started to define functional big-step semantics for the Dafny IR to prove correctness of the backend.