A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
From MaRDI portal
Publication:3613425
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
