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.


翻译:最近有人有兴趣用证据助理来核查monaddic程序。 这一研究线索提出了monad变压器的集成问题,这是将monad变压器结合在一起的一种标准技术。 在本文中,我们扩展了Monae,这是一个用monad变压器进行monadic等式推理的 Coq 图书馆,我们用monad变压器来解释这一扩展的好处。我们的出发点是模块monad变压器的现有理论,它提供了对操作的统一处理。我们利用这一理论,简化了Monae 模型的正规化,我们提出了一个方法,支持monad变压器出现时的monad 等式推理。我们还利用Monae 重新审视模块moad变压器的提法,提供方程式证据,并解释如何使用非标准使用的Coq来修补已知的虫,将不合理的多形态和对称性结合起来。

0
下载
关闭预览

相关内容

最新《Transformers模型》教程,64页ppt
专知会员服务
305+阅读 · 2020年11月26日
最新《生成式语言模型: 信息论视角》报告,292页ppt
专知会员服务
28+阅读 · 2020年11月9日
【机器推理可解释性】Machine Reasoning Explainability
专知会员服务
34+阅读 · 2020年9月3日
Transformer文本分类代码
专知会员服务
116+阅读 · 2020年2月3日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
CCF推荐 | 国际会议信息10条
Call4Papers
8+阅读 · 2019年5月27日
人工智能 | NIPS 2019等国际会议信息8条
Call4Papers
7+阅读 · 2019年3月21日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
【推荐】决策树/随机森林深入解析
机器学习研究会
5+阅读 · 2017年9月21日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
Arxiv
0+阅读 · 2021年5月12日
Arxiv
0+阅读 · 2021年5月10日
Arxiv
0+阅读 · 2021年5月6日
Arxiv
23+阅读 · 2020年9月16日
Arxiv
6+阅读 · 2018年1月29日
VIP会员
相关论文
Arxiv
0+阅读 · 2021年5月12日
Arxiv
0+阅读 · 2021年5月10日
Arxiv
0+阅读 · 2021年5月6日
Arxiv
23+阅读 · 2020年9月16日
Arxiv
6+阅读 · 2018年1月29日
Top
微信扫码咨询专知VIP会员