LF元理论的机械化
Mechanizing the Metatheory of LF
摘要：
LF是一个依赖的类型论，许多其他形式系统可以方便地嵌入其中。然而，正确使用LF依赖于非平凡的元理论的发展，如证明LF的判断决策程序的正确性。虽然这些性质的详细的非正式证明已经公布，他们还没有正式验证的定理证明。我们已经在Isabelle/HOL中使用Nominal Datatype Package正式定义了这些属性，紧跟Harper和Pfenning最近的一篇文章。在这个过程中，我们发现并解决了其中一个证明中的一个缺口，以及其他证明中的一些小缺陷。我们还正式推导出一个版本的类型检查算法，Isabelle/HOL可以生成可执行代码。除了它的内在利益，我们的形式化提供了一个基础，研究LF编码的充分性，BURMF式元理论推理的正确性，和元理论的LF扩展。
英文摘要：
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the Nominal Datatype Package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. We also formally derive a version of the type checking algorithm from which Isabelle/HOL can generate executable code. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
