Abstract
Computing efficiently with numbers can be crucial for some theorem proving applications. In this paper, we present a library of modular arithmetic that has been developed within the COQ proof assistant. The library proposes the usual operations that have all been proved correct. The library is purely functional but can also be used on top of some native modular arithmetic. With this library, we have been capable of certifying the prirnality of numbers with more than 13000 digits. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Grégoire, B., & Théry, L. (2006). A purely functional library for modular arithmetic and its application to certifying large prime numbers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4130 LNAI, pp. 423–437). Springer Verlag. https://doi.org/10.1007/11814771_36
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
