精化反射（或者，如何使用SMT将您喜爱的语言转换为证明助手）
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)
摘要：
Refinement Reflection通过将实现用户定义函数的代码反映到函数的（输出）细化类型中，将您最喜欢的程序设计语言变成一个证明助手。因此，在函数的使用中，函数定义以精确的、可预测的、最重要的是程序员可控的方式展开到细化逻辑中。在逻辑中，我们使用未解释的符号编码的功能，并保留基于SMT的可判定性验证。在该语言中，我们提供了一个组合子库，让程序员可以从基本的改进和函数定义中组合证明。我们已经在Liquid Haskell系统中实现了我们的方法，从而将Haskell转换为一个交互式证明助手，我们用来验证各种属性，从高阶的算术属性，递归函数到Monoid，Application，Functor和Monad类型的类法律的各种实例。
英文摘要：
Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is unfolded into the refinement logic in a precise, predictable and most importantly, programmer controllable way. In the logic, we encode functions and lambdas using uninterpreted symbols preserving SMT-based decidable verification. In the language, we provide a library of combinators that lets programmers compose proofs from basic refinements and function definitions. We have implemented our approach in the Liquid Haskell system, thereby converting Haskell into an interactive proof assistant, that we used to verify a variety of properties ranging from arithmetic properties of higher order, recursive functions to the Monoid, Applicative, Functor and Monad type class laws for a variety of instances.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
