基于逻辑框架LF的语义性质之验证

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