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

摘要：

@@ 1.引言近些年来,在计算机程序设计语言理论、自动演绎以及更一般的逻辑和计算领域研究中,出现了多种以构造类型论为基础的系统,如LCF、ALF、LEGO、Coq等,它们被用来为程序设计语言设计类型系统,进行程序开发和验证、形式化证明以及作为数学和计算的基础.构造类型论为计算机科学家提供了一个框架,以一种优雅和灵活的方式把逻辑和程序设计语言结合起来:在同一形式系统中,可以同时表达规约和(函数式语言)程序,从证明规则可以导出正确的程序,并验证程序具有某种性质,从而在同一系统内完成程序的开发和验证[26,19].

机标关键词：构造、类型论、计算机、程序设计语言、形式系统、验证程序、形式化证明、函数式语言、证明规则、语言设计、语言理论、逻辑、类型系统、程序开发、基础、科学家、种性、演绎、数学、框架

所属期刊栏目：29

分类号：TP31(计算技术、计算机技术)

资助基金：国家自然科学基金69931040;国防科研项目GF00J6.2.1.JB0501

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：72-77,61