【摘要】 构造性类型理论可作为程序开发的理论基础，其中类型作为程序规约，证明过程作为程序开发过程，从证明抽取满足程序规约的程序．本文提出了一种构造性类型理论ＴＴＯＯＰ，引入了类规约类型和类类型的概念．类是类规约类型的元素，它又是一种类型，类的元素为对象．通过证明类规约可构造类，由此构造面向对象软件．更多还原

【Abstract】 A constructive type theory TTOOP, in which the concept of class specification type and class type are introduced, is proposed in this paper. Class is an element of the class specification type, and the elements of the class type are the objects. By proving class specifications, classes can be constructed and the object--oriented software can be constructed with these classes.更多还原