Mechanisation of the AKS algorithm
DOI10.1007/s10817-020-09563-yzbMath1465.68301OpenAlexW3081717911MaRDI QIDQ2031415
Michael Norrish, Hing-Lun Chan
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09563-y
computational complexityfinite fieldsautomated reasoningnumber theorymachine modeltheorem-provingAKS algorithmwriter monad
Analysis of algorithms and problem complexity (68Q25) Number-theoretic algorithms; complexity (11Y16) Mechanization of proofs and logical operations (03B35) Factorization; primality (11A51) Primality (11Y11) Formalization of mathematics in connection with theorem provers (68V20)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- FST TCS 2002: Foundations of software technology and theoretical computer science. 22nd conference, Kanpur, India, December 12--14, 2002. Proceedings
- Verification of the Miller-Rabin probabilistic primality test.
- Proof pearl: Bounding least common multiples with triangles
- PRIMES is in P
- Automated higher-order complexity analysis
- Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P.
- Classification of finite fields with applications
- Hoare logics for time bounds. A study in meta theory
- Proving divide and conquer complexities in Isabelle/HOL
- Modern Computer Algebra
- Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
- Analysing the complexity of functional programs: higher-order meets first-order
- Proving Pearl: Knuth’s Algorithm for Prime Numbers
- Four primality testing algorithms
- On Chebyshev-Type Inequalities for Primes
- A String of Pearls: Proofs of Fermat's Little Theorem
- Automated Reasoning
This page was built for publication: Mechanisation of the AKS algorithm
