论文标题
使用单子变压器扩展方程式元素推理
Extending Equational Monadic Reasoning with Monad Transformers
论文作者
论文摘要
最近，使用证明助手验证了Monadic计划。这一研究提出了单个变形金刚的整合问题，这是一种结合单元的标准技术。在本文中，我们扩展了Monade式推理的COQ库Monae，并使用Monad Transformers扩展了该文档，并解释了这一扩展的好处。我们的起点是现有的模块化单变压器的理论，该理论提供了对操作的统一处理。使用该理论，我们简化了Monae中模型的形式化，并提出了一种支持单纳德变形金刚在存在的模型方程推理的方法。我们还使用Monae通过提供方程证明并解释了如何使用非标准的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.
