A computational approach to pocklington certificates in type theory

Benjamin Grégoire; Laurent Théry; Benjamin Werner

doi:10.1007/11737414_8

A computational approach to pocklington certificates in type theory

Benjamin Grégoire
, Laurent Théry
, Benjamin Werner

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 (two-level approach).

Original language	English
Title of host publication	Functional and Logic Programming
Subtitle of host publication	8th International Symposium, FLOPS 2006, Proceedings
Publisher	Springer Verlag
Pages	97-113
Number of pages	17
ISBN (Print)	3540334386, 9783540334385
DOIs	https://doi.org/10.1007/11737414_8
Publication status	Published - 1 Jan 2006
Externally published	Yes
Event	8th International Symposium on Functional and Logic Programming, FLOPS 2006 - Fuji-Susono, Japan Duration: 24 Apr 2005 → 26 Apr 2005

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3945 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	8th International Symposium on Functional and Logic Programming, FLOPS 2006
Country/Territory	Japan
City	Fuji-Susono
Period	24/04/05 → 26/04/05

Access to Document

10.1007/11737414_8

Cite this

Grégoire, B., Théry, L., & Werner, B. (2006). A computational approach to pocklington certificates in type theory. In Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Proceedings (pp. 97-113). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3945 LNCS). Springer Verlag. https://doi.org/10.1007/11737414_8

Grégoire, Benjamin ; Théry, Laurent ; Werner, Benjamin. / A computational approach to pocklington certificates in type theory. Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Proceedings. Springer Verlag, 2006. pp. 97-113 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d7b867f2793a4087902091cdc6cb087e,

title = "A computational approach to pocklington certificates in type theory",

abstract = "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 (two-level approach).",

author = "Benjamin Gr{\'e}goire and Laurent Th{\'e}ry and Benjamin Werner",

year = "2006",

month = jan,

day = "1",

doi = "10.1007/11737414\_8",

language = "English",

isbn = "3540334386",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "97--113",

booktitle = "Functional and Logic Programming",

note = "8th International Symposium on Functional and Logic Programming, FLOPS 2006 ; Conference date: 24-04-2005 Through 26-04-2005",

}

Grégoire, B, Théry, L & Werner, B 2006, A computational approach to pocklington certificates in type theory. in Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3945 LNCS, Springer Verlag, pp. 97-113, 8th International Symposium on Functional and Logic Programming, FLOPS 2006, Fuji-Susono, Japan, 24/04/05. https://doi.org/10.1007/11737414_8

A computational approach to pocklington certificates in type theory. / Grégoire, Benjamin; Théry, Laurent; Werner, Benjamin.
Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Proceedings. Springer Verlag, 2006. p. 97-113 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3945 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A computational approach to pocklington certificates in type theory

AU - Grégoire, Benjamin

AU - Théry, Laurent

AU - Werner, Benjamin

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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 (two-level approach).

AB - 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 (two-level approach).

UR - https://www.scopus.com/pages/publications/33745850404

U2 - 10.1007/11737414_8

DO - 10.1007/11737414_8

M3 - Conference contribution

AN - SCOPUS:33745850404

SN - 3540334386

SN - 9783540334385

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 97

EP - 113

BT - Functional and Logic Programming

PB - Springer Verlag

T2 - 8th International Symposium on Functional and Logic Programming, FLOPS 2006

Y2 - 24 April 2005 through 26 April 2005

ER -

Grégoire B, Théry L, Werner B. A computational approach to pocklington certificates in type theory. In Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Proceedings. Springer Verlag. 2006. p. 97-113. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11737414_8

A computational approach to pocklington certificates in type theory

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this