摘要： Recent years,in the area of computer programming language theories,automated deduction,and more generalized area of logic and computing,a lot of systems based on constructive type theory are used widely to design type system for computer programming langu

关键词: 限制谓词演算 构造类型论 构造数学 计算机 程序设计 程序设计语言