Encoding Lean's Type Theory in Dedukti
En palabras de los autores
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.
Resultado principalLimitación que admiten los autores
Apareció: martes, 22 de septiembre. arXiv. Preprint con versión publicada.
Versión publicada: ICTAC 2026 - International Colloquium on Theoretical Aspects of Computing, Nov 2026, Bariloche, Argentina