Mechanisation of the AKS algorithm
type: Item
instance of: scholarly article
title: Mechanisation of the AKS algorithm
zbMATH Open document ID: 1465.68301
author: Michael Norrish
author: Hing-Lun Chan
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 11A51
Mathematics Subject Classification ID: 11Y11
Mathematics Subject Classification ID: 11Y16
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 7356972
zbMATH Keywords: theorem-proving
zbMATH Keywords: automated reasoning
zbMATH Keywords: AKS algorithm
zbMATH Keywords: number theory
zbMATH Keywords: finite fields
zbMATH Keywords: computational complexity
zbMATH Keywords: writer monad
zbMATH Keywords: machine model
describes a project that uses: Isabelle
describes a project that uses: PURRS
describes a project that uses: ACE
describes a project that uses: HOL
describes a project that uses: Isabelle/HOL
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: s10817-020-09563-y
OpenAlex ID: W3081717911
cites work: PRIMES is in P
cites work: Analysing the complexity of functional programs: higher-order meets first-order
cites work: Automated Reasoning
cites work: Automated higher-order complexity analysis
cites work: Q4826696
cites work: A String of Pearls: Proofs of Fermat's Little Theorem
cites work: Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
cites work: Classification of finite fields with applications
cites work: Proof pearl: Bounding least common multiples with triangles
cites work: Q5317673
cites work: Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P''.
cites work: Proving divide and conquer complexities in Isabelle/HOL
cites work: Hoare logics for time bounds. A study in meta theory
cites work: Verification of the Miller-Rabin probabilistic primality test.
cites work: Q4349924
cites work: FST TCS 2002: Foundations of software technology and theoretical computer science. 22nd conference, Kanpur, India, December 12--14, 2002. Proceedings
cites work: On Chebyshev-Type Inequalities for Primes
cites work: Primality testing for beginners. Translated from the German
cites work: Four primality testing algorithms
cites work: Proving Pearl: Knuth’s Algorithm for Prime Numbers
cites work: Modern computer algebra
DOI: 10.1007/S10817-020-09563-Y
description: scientific article; zbMATH DE number 7356972