1 citations · 2 across the 3 of their papers we have counts for
3 papers
cs.LO2022★ 1 cited
Revisiting the Fast Fourier Transform in Rocq
Laurent Théry
This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect ex…
cs.LO2022★ 1 cited
Primality Tests and Prime Certificate
Laurent Théry, Sophia Antipolis
This note presents a formalisation done in Coq of Lucas-Lehmer test and Pocklington certificate for prime numbers. They both are direct consequences of Fermat little theorem. Ferma…
cs.DS2022
A Formalisation of Algorithms for Sorting Network
Laurent Théry
This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.