ATS: a Language to Support Practical Programming with Theorem Proving

提案编号：CCF-0702665标题：ATS：一种支持定理证明的实用编程语言PI：Hongwei Xi软件设计和实现的巨大复杂性是显而易见的。 在当今时代，软件设计通常以不同程度的形式主义形式表达，从口头讨论到纯文本描述，再到UML图，再到Z等语言的规格说明。 此外，在系统的设计和实际实现之间往往存在巨大的差距，这使得构建符合其规范的软件变得非常困难。 然而，构建满足其规范的软件的能力对于（高度）可靠的计算至关重要，并且似乎没有其他捷径。 建议的研究重点是设计和实现一个成熟的编程语言ATS的类型系统植根于最近开发的框架应用类型系统。在ATS中，软件设计中的（某些）规范可以根据类型形式化地捕获，然后通过类型检查进行验证。 与从证明中提取程序的纯定理证明系统形成鲜明对比的是，ATS是一种有效的编程语言，它包含一个纯定理证明子系统来支持具有定理证明的编程。ATS的有效性要在构建真实的复杂系统中进行评估。

Proposal Number: CCF-0702665TITLE: ATS: A Language to Support Practical Programming with Theorem ProvingPI: Hongwei XiThe immense complexity in software design and implementation is evident. In this day and age, software design is often expressed in forms of varying degree of formalism, ranging from verbal discussions to plain text descriptions to UML diagrams to specifications in languages like Z. Also, there is often an enormous gap between the design of a system and its actual implementation, making it exceedingly difficult to construct software meeting its specification. However, the very ability to construct software meeting its specification is crucial to (highly) dependable computing, and there seem to be no other shortcuts. The proposed research focuses on the design and implementation of a full-fledged programming language ATS with a type system rooted in the recently developed framework Applied Type System. In ATS, (certain) specifications in software design can be formally captured in terms of types and then be verified through type-checking. In stark contrast to pure theorem proving systems where programs are extracted from proofs, ATS is an effective programming language that contains a pure theorem-proving subsystem to support programming with theorem proving. The effectiveness of ATS is to be evaluated in the construction of real and complex systems.