DSLean：一种用于Lean 4与外部DSL之间类型正确的互操作框架
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
AI总结：
DSLean是一种用于Lean 4与外部DSL之间类型正确互操作的框架，通过双向翻译实现与外部求解器的高效交互。
摘要：
领域特定语言（DSLs）在交互式证明助手和外部自动化之间起中介作用，但将证明器的内部表示与这些DSL进行翻译是一项繁琐的工程任务。为了简化这一任务，我们提出了DSLean，一种用于在Lean证明助手和外部语法之间进行双向翻译的框架。DSLean只需指定外部语言及其Lean等价物的规范，抽象掉元级实现细节。我们通过实现三个新的自动化战术来展示DSLean的能力，为区间算术、常微分方程和环理想成员资格提供对外部求解器的访问。
英文摘要：
Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
