模块化类型-使用依赖类型的安全性证明
Modular Type-Safety Proofs using Dependant Types
摘要：
虽然代码抽象和重用的方法已经广泛应用并得到了很好的研究，但证明抽象和重用的方法仍然在不断涌现。我们考虑使用依赖类型为这个目的，介绍了一个完全机械的方法证明组合。我们发现，一般的技术抽象算法的数据结构自然转化为抽象证明。我们首先介绍一种由一系列较小的语言组件组成的语言，这些组件通过Malcom（1990）的标准技术联系在一起。我们继续给每个语言组件的类型保持的证明，并表明，在组成的语法数据结构的基本思想可以适用于它们的语义。
英文摘要：
While methods of code abstraction and reuse are widespread and well researched, methods of proof abstraction and reuse are still emerging. We consider the use of dependent types for this purpose, introducing a completely mechanical approach to proof composition. We show that common techniques for abstracting algorithms over data structures naturally translate to abstractions over proofs. We first introduce a language composed of a series of smaller language components tied together by standard techniques from Malcom (1990). We proceed by giving proofs of type preservation for each language component and show that the basic ideas used in composing the syntactic data structures can be applied to their semantics as well.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
