Verification of Semantic Properties Based on Logical Framework
基于逻辑框架LF的语义性质之验证

本文对基于类型理论逻辑框架（LF）的语义性质验证加以研究，针对函数式语言LAZY-PCF＋SHAR，利用计算机辅助推理方法和技术给出相应的形式化描述及相关性质证明，从而提倡严格的和计算机辅助的证明在语义性质验证方面的应用。同时，考察了LF以及其实现系统Plastic的能力。