首页> 外文期刊>Programming and Computer Software >On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
【24h】

On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain

机译:在GCD域上的分数算法的机器检查证明

获取原文
获取原文并翻译 | 示例

摘要

In this paper, we describe design principles for certified programs of fraction arithmetic over any domain with the greatest common divisor (GCD) function. This is a small part of the DoCon-A library of certified programs, which is designed by the author of this paper. In this system, programs include definitions of the corresponding mathematical notions and proofs for the main properties of the methods implemented. These proofs are checked by the compiler. A purely functional programming language Agda, which supports dependent types, is used. A technique to generate formal machine-checked proofs for a certain optimized method of fraction addition is described.
机译:在本文中,我们描述了在任何具有最大域(GCD)功能的域上的任何域上的分数算法的认证程序的设计原则。这是Docon的一小部分 - 通过本文的作者设计了认证计划的库。在该系统中,程序包括相应的数学概念的定义和实现的方法的主要属性。这些证明由编译器检查。使用支持依赖类型的纯粹功能编程语言AGDA。描述了一种用于产生一定优化的分数加法方法的正式机器检查证据。

著录项

  • 来源
    《Programming and Computer Software》 |2020年第2期|110-119|共10页
  • 作者

    Meshveliani S. D.;

  • 作者单位

    Russian Acad Sci Ailamazyan Program Syst Inst Ul Petra Pervogo 4a Pereslavsky Dist 152021 Yaroslavl Oblas Russia;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号