发表机构
INRIA; ENS Paris-Saclay; CNRS（法国国家信息与自动化研究所; 巴黎萨克雷高等师范学院; 法国国家科学研究中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出在Dedukti逻辑框架中编码Lean类型论的理论，并定义从Lean大子集到该理论的保持可类型化的翻译，以促进Lean库向其他系统的转换。
AI 中文摘要
Lean证明助手拥有丰富的数学形式化库，这对其他证明助手的用户很有吸引力。为了帮助将该库翻译到其他系统，我们在Dedukti逻辑框架中提出了一种理论，该理论可以编码Lean的项和类型，并定义了从Lean的某个大子集到该Dedukti理论的保持可类型化的翻译。
英文摘要
The Lean proof assistant has a rich library of mathematical formalizations that are interesting to users of other proof assistants. To help with the translation of this library to other systems, we present a theory in the Dedukti logical framework in which one can encode Lean terms and types, and define a typability-preserving translation from some large subset of Lean to that Dedukti theory.
Journal refICTAC 2026 - International Colloquium on Theoretical Aspects of Computing, Nov 2026, Bariloche, Argentina
