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

摘要

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.