减少编程错误：基于认证内核的全新的快捷依赖类型PiSigma高级编程语言开发

我们将会把最近的一些研究成果整合在一起用以开发一个更有效率的基于依赖类型论的高级函数编程语言。我们现在称这个语言为PiSigma 语言，该语言的开发将建立于一个由我们的实验室开发的已经认证的优雅的内核设计的基础上来完成的。依赖类型编程语言现在已被公认为保证软件安全及攻克软件工程难题的关键技术，同时它也是近期同类型研究的核心技术。该语言将会在很大程度上减少软件开发人员出现的运行错误，同时也会在很大程度上使认证关键应用程序的工作变得简单。.我们的目标是将尖端理论研究转化为实用、受欢迎的软件工程工具。为达此目标，我们也将开发一个现代的编程平台，以帮助软件工程师迅速并安全地开发新应用程序，尤其是透过特殊领域程序库，隐性语法，范用编程，样式配对等技术。. 同时该项目的一个重要战略是壮大我们的研究组织在中国分支的力量，进而吸引更多的国际知名学者加入到我们当中来，和我们一起在中国开展更。

最初的项目是基于构造类型论，实现一个不仅允许定义类型依赖方程（并带有自动类型检查器），而且允许编写构造式证明（并带有自动正确性校验）的编程语言。最初的项目的主要部分已经完成，并伴有近期发表的有关与附着于该语言的数学实数分析模块的理论成果（Farjudian2014a，B，C），或有助于我们探索在该语言中构造一个对其自身核心正确性的证明。然而事实证明，这最后的一点比预先料想的更有难度，并不能很快做到。尽管该项目曾由于工作人员离开项目以及用了很长时间才发现的漏洞（bug）停滞了一段时间，我们还是成功地克服了该语言中最困难的部分，并且该语言已进入beta测试。该项目的其他几个次要的部分，如集成开发环境的开发或文档库的编写，将在未来的工作予以实现（见下文的甘特图表）。