A Why3 proof of GMP algorithms

Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. J. Formalized Reasoning, 12(1):53-97, 2019. [doi]

@article{Rieu-Helft19,
  title = {A Why3 proof of GMP algorithms},
  author = {Raphaël Rieu-Helft},
  year = {2019},
  doi = {10.6092/issn.1972-5787/9730},
  url = {https://doi.org/10.6092/issn.1972-5787/9730},
  researchr = {https://researchr.org/publication/Rieu-Helft19},
  cites = {0},
  citedby = {0},
  journal = {J. Formalized Reasoning},
  volume = {12},
  number = {1},
  pages = {53-97},
}