类型理论和程序设计

Type Theory and Programming

一、类型理论的起源与发展类型理论的基本思想和方法学基础来源于哲学中的归类(classification)方法,即把具有共同特点的类集合成超类的思维过程和方法。归类是形成概念的先决条件之一,分类方法在认识和实践活动中有广泛的应用。

Type theory is a formalism which studies the principles of typedefinitions and deductions.It is currently one of the most activeareas in computer science.This paper gives a survey of the originand development of type theory.The relationships among type theory,logics and algebras are discussed and some distinguished type systemsare introduced.We put emphasis on the applications of type theory toprogramming languages and software development.