A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers

DOI10.1007/11814771_36zbMath1222.68363OpenAlexW1652609218MaRDI QIDQ3613425

Benjamin Grégoire, Laurent Théry

Publication date: 12 March 2009

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11814771_36

Mathematics Subject Classification ID

Primes (11A41) Primality (11Y11)

Related Items (6)

Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Enabling floating-point arithmetic in the Coq proof assistant ⋮ Proving Bounds on Real-Valued Functions with Computations ⋮ A certificate-based approach to formally verified approximations ⋮ Primitive Floats in Coq ⋮ Floating-point arithmetic in the Coq system

Uses Software

• Coq
• OCaml

This page was built for publication: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers