论文标题
Syntheto：APT和ACL2的表面语言
Syntheto: A Surface Language for APT and ACL2
论文作者
论文摘要
Syntheto是一种表面语言，用于使用APT Toolkit在ACL2中进行变换的改进，以进行正式验证的程序合成。 Syntheto的目的是提供更多的熟悉和自动化，以使该技术更广泛地使用。 Syntheto是一种强烈静态键入的功能语言，包括可执行文件和不可执行的构造，包括陈述的设施并证明定理和设施以应用证据生成的转换。 Syntheto与笔记本风格的交互式接口集成到IDE中，该界面将Syntheto转换为ACL2定义和APT Transformation Inconcations，并将供摊子的结果反转换为Syntheto；双向翻译发生在幕后，用户仅与Syntheto进行交互。
Syntheto is a surface language for carrying out formally verified program synthesis by transformational refinement in ACL2 using the APT toolkit. Syntheto aims at providing more familiarity and automation, in order to make this technology more widely usable. Syntheto is a strongly statically typed functional language that includes both executable and non-executable constructs, including facilities to state and prove theorems and facilities to apply proof-generating transformations. Syntheto is integrated into an IDE with a notebook-style, interactive interface that translates Syntheto to ACL2 definitions and APT transformation invocations, and back-translates the prover's results to Syntheto; the bidirectional translation happens behind the scenes, with the user interacting solely with Syntheto.
