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.