系统FR作为不锈钢的基础
System FR as Foundations for Stainless
摘要：
我们提出的设计，实现和基础的验证高阶函数程序的泛型和递归数据类型。我们的系统支持证明安全性和终止使用的前提条件，后置条件和断言。它支持使用断言和递归调用编写证明提示。为了形式化系统的可靠性，我们引入了系统FR，一个支持系统F多态性、依赖细化类型和递归类型（包括通过函数类型的逆变位置的递归）的演算。通过使用大小类型，系统FR支持有关惰性数据结构（如流）终止的推理。我们正式减少使用Coq证明助手的参数，并证明了一个类型检查器的可靠性，按值调用语义，确保类型安全和规范化的可类型程序。我们的程序验证器实现为Stainless工具的替代验证条件生成器，该工具依赖于现有的基于SMT的求解器后端进行自动化。我们证明了我们的方法的效率，通过验证一系列高阶函数程序，包括约14000行多态高阶Scala代码，包括图搜索算法，基本数论，单子定律，功能数据结构，并从流行的函数编程MOOC的任务。
英文摘要：
We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and assertions. It supports writing proof hints using assertions and recursive calls. To formalize the soundness of the system we introduce System FR, a calculus supporting System F polymorphism, dependent refinement types, and recursive types (including recursion through contravariant positions of function types). Through the use of sized types, System FR supports reasoning about termination of lazy data structures such as streams. We formalize a reducibility argument using the Coq proof assistant and prove the soundness of a type-checker with respect to call-by-value semantics, ensuring type safety and normalization for typeable programs. Our program verifier is implemented as an alternative verification-condition generator for the Stainless tool, which relies on existing SMT-based solver backend for automation. We demonstrate the efficiency of our approach by verifying a collection of higher-order functional programs comprising around 14000 lines of polymorphic higher-order Scala code, including graph search algorithms, basic number theory, monad laws, functional data structures, and assignments from popular Functional Programming MOOCs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
