@MISC{NTALGO_1.MIZ,
  AUTHOR = {Okazaki, Hiroyuki and Aoki, Yosiki and Shidama, Yasunari},
  TITLE = {Extended Euclidean Algorithm and CRT Algorithm},
  SECTION1 = {Euclidean Algorithm},
  SECTION2 = {Extended Euclidean Algorithm},
  SECTION3 = {CRT Algorithm},
  DAY = {8},
  MONTH = {February},
  YEAR = {2012},
  ADDRESS1 = {Shinshu University, Nagano, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  ADDRESS3 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {In this article, we formalize some number theoretical algorithms,
  Euclidean Algorithm and Extended Euclidean Algorithm \cite{Knuth2}.
  Besides the a gcd b, Extended Euclidean Algorithm
  can calculate a pair of two integers (x,y) that holds ax+by = a gcd b.
  In addition, we formalize  an algorithm that can compute
  a solution of the chinese reminder theorem by using Extended Euclidean
  Algorithm.
  Our aim is to support implementation of number theoretic tools.
  Our formalization of those algorithms are based on the source code of
  the NZMATH, a number theory oriented calculation system developed by
  Tokyo Metropolitan University \cite{NZMATH}.},
  ACKNOWLEDGEMENT = {This work was supported by
  JSPS KAKENHI 2124000101 and 22300285.}}

@BOOK{Knuth2,
      AUTHOR = {Donald E. Knuth},
      TITLE = {Art of Computer Programming, Volume 2: Seminumerical Algorithms 3rd Edition},
      PUBLISHER = {Addison-Wesley Professional},
      YEAR = {1997}}

ARTICLE{NZMATH,
      AUTHOR  = {NZMATH development Group},
      TITLE   = {NZMATH http://tnt.math.se.tmu.ac.jp/nzmath/}}
