Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a new imperative programming language whose design is grounded in a static type system that ensures the following equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some programs of the language. The contribution of this work is twofold. On the theoretical side, the foundational equivalence property is established, and the proof of the equivalence theorem is non-trivial. On the practical side, a programming approach is proposed that can streamline program analysis and verification for feasible computations. An interpreter for the language has been implemented, demonstrating the feasibility of the approach in practice.

翻译：运行时效率和程序终止是程序验证研究中的关键属性。与其以临时方式处理这些问题，更可取的是开发一个稳健的框架，在这些框架中，此类性质通过设计得以保证。本文介绍了一种新的命令式程序设计语言，其设计基于一个静态类型系统，该系统确保以下等价性质：所有可定义的程序都保证在多项式时间内运行；反之，所有可在多项式时间内求解的问题都能通过该语言的某些程序得到解决。本工作的贡献体现在两个方面。在理论方面，建立了基础的等价性质，且等价定理的证明非同寻常。在实践方面，提出了一种程序设计方法，能够简化可行计算的程序分析与验证。该语言的解释器已实现，证明了该方法在实践中的可行性。