逻辑类型理论的语义及其应用

本项目有以下几个方面的研究成果：一、给出了构造集合论在可判定马丁诺夫系统中的解释，提供了构造集合论在计算机上实现的一条途径。二、构造了带有广义归纳类型的构造演算的ω集模型。为在构造演算中进行程序规范说明和程序构造找到了语义解释。三、使用范畴论给出了逻辑框架的二层语义，该语义对如何在逻辑框架中正确地定义逻辑有启发意义。四、提出并研究一新型并发计算模型：π－演算。使演算比π－演算更简单、表达能力更强。