Sciweavers

FLOPS
2006
Springer

A Computational Approach to Pocklington Certificates in Type Theory

14 years 3 months ago
A Computational Approach to Pocklington Certificates in Type Theory
Pocklington certificates are known to provide short proofs of primality. We show how to perform this in the framework of formal, mechanically checked, proofs. We present an encoding of certificates for the proof system Coq which yields radically improved performances by relying heavily on computations inside and outside of the system (twolevel approach). 1 Formal Computational Proofs
Benjamin Grégoire, Laurent Théry, Be
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FLOPS
Authors Benjamin Grégoire, Laurent Théry, Benjamin Werner
Comments (0)