构造类型论与计算机程序设计

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 languages,to do formal system develpment and verification,and to be used as foundation of mathematics and computing.constructive type theory provides computer scientists with a framework to combine logic and computer program design in an elegant and flexible way.In this paper,the evolvement of constructive type theory is first introduced.The several foundations of type theory are then discussed,together with analysis of the relationships between them.The relation between constructive type theory and computer programming is explored in-depth.In the last,Martin Lof‘‘‘‘s intuitionistic type theory is used as an example to demonstrate how to do program development and verification in the same formal system.

Type System and Computer Programming