CAREER: Realistic Program Termination Verification: Theory and Practice

这个职业生涯项目结合了一个研究组成部分-设计一个实用的方法来程序终止验证，包括理论研究和实际实施-与教育组成部分-进行增强，为本科生和研究生，编程语言教育。 终止验证的研究认识到，在实践中，程序员往往知道由于某些原因，一个特定的程序应该终止，如果正确实现，因此会发现很大的价值，在终止检查器能够检测程序错误，导致非终止程序执行。 不幸的是，在支持一般递归的编程语言中，终止检查的开销通常非常大。 为了设计一个实际使用的终止检查器，该项目探讨了在实际编程中使用依赖类型的一些最新结果，允许程序员将确保程序终止所需的度量编码为依赖类型，然后使用类型检查来验证所提供的度量确实足够。 研究的重点是提供一种真正可以在实践中应用的机制。

This CAREER project combines a research component--designing a practical approach to program termination verification that includes both theoretical study and actual implementation--with an educational component--undertaking the enhancement, for both undergraduates and graduates, of programming language education. The research on termination verification recognizes that, in practice, the programmer often knows for some reasons that a particular program should terminate if implemented correctly and would therefore find great value in a termination checker able to detect program errors that cause non-terminating program execution. Unfortunately, termination checking in a programming language that supports general recursion is often prohibitively expensive. In order to design a termination checker for practical use, the project explores some recent results on the use of dependent types in practical programming, allowing the programmer to encode into dependent types the metrics needed for ensuring program termination and then use type-checking to verify that the provided metrics indeed suffice. The research focuses on providing a mechanism that truly can be applied in practice.