用单子Transformers扩展等式单子推理
Extending Equational Monadic Reasoning with Monad Transformers
摘要：
最近有兴趣验证一元程序使用证明助手。这一系列的研究提出了整合monad Transformers的问题，这是一种组合monad的标准技术。在本文中，我们扩展Monae，一个一元方程推理的Coq库，与单子Transformers，我们解释了这种扩展的好处。我们的出发点是现有的理论模块单子Transformers，它提供了一个统一的处理操作。利用这一理论，我们简化了形式化的模型在Monae，我们提出了一种方法来支持一元方程推理的单子Transformers的存在。我们还使用Monae来重新审视模块化单子Transformers的提升定理，通过提供等式证明并解释如何使用Coq的非标准使用来修补已知的错误，该Coq结合了非谓词多态性和参数性。
英文摘要：
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
