• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>8th International Workshop on Computer Aided Systems Theory, 8th, Feb 19-23, 2001, Las Palmas de Gran Canaria, Spain >Fusion in Coq
【24h】

Fusion in Coq

机译：Coq中的融合

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Fusion theorem is a classical result that allows the simplification of the morphisms among homogeneus structures. We present this theorem and some generalizations in the context of the constructive proof assistant tool Coq where we have dependent types and parametric polymorphism. The work is organised as follows: afther the classical interpretation of the fusion law for catamorphisms in a categoric context, examples of fusion for programs defined with recursive types in Coq are analysed and the theorems of corresponding optimisation are shown. Finally, a generalisation of fusion law for inductive types is presented which is applied to a specific case.
机译：融合定理是一个经典的结果，它可以简化同质结构之间的形态。我们在构造性证明辅助工具Coq的上下文中介绍该定理和一些概括，其中我们具有从属类型和参数多态性。这项工作的组织如下：在分类上下文中对同态同构融合定律的经典解释之后，分析了在Coq中用递归类型定义的程序的融合实例，并显示了相应的优化定理。最后，对归纳类型的融合定律进行了概括，并将其应用于特定情况。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号