Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

17

FLOPS
2006
Springer

favoriteEmaildiscussreport

119views Automated Reasoning» more FLOPS 2006»

A Computational Approach to Pocklington Certificates in Type Theory

13 years 8 months ago

A Computational Approach to Pocklington Certificates in Type Theory

Download www-sop.inria.fr

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

Real-time Traffic

Automated Reasoning | FLOPS 2006 | Formal Computational Proofs | Pocklington Certificates | Short Proofs |

claim paper

Related Content

» Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory

» A computational approach to reflective metareasoning about languages with bindings

» Passwords youll never forget but cant recall

» Towards Computability of Higher Type Continuous Data

» Theory Interpretation in Simple Type Theory

» Certification and Authentication of Data Structures

» A computable approach to measure and integration theory

» Fundamental Theory for Typed Attributed Graph Transformation

» The Suslin operator in applicative theories Its prooftheoretic analysis via ordinal theori...

Post Info
More Details (n/a)

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)