meta.yml

---
fullname: Pocklington
shortname: pocklington
organization: coq-community
community: true
action: true
nix: true
coqdoc: false

synopsis: Pocklington's criterion for primality in Coq

description: |-
  Coq formalization of Pocklington's criterion for checking primality of
  large natural numbers. Includes a formal proof of Fermat's little theorem.

publications:
- pub_url: https://core.ac.uk/download/pdf/82730602.pdf
  pub_title: Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles
  pub_doi: 10.1006/jsco.2001.0457

authors:
- name: Olga Caprotti
  initial: true
- name: Martijn Oostdijk
  initial: true

maintainers:
- name: Pierre Castéran
  nickname: Casteran

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later

supported_coq_versions:
  text: 8.7 or later
  opam: '{(>= "8.7" & < "8.17~") | (= "dev")}'

tested_coq_opam_versions:
- version: dev
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'
- version: '8.9'
- version: '8.8'
- version: '8.7'

tested_coq_nix_versions:
- coq_version: master

namespace: Pocklington

keywords:
- name: Pocklington
- name: number theory
- name: prime numbers
- name: primality
- name: Fermat's little theorem

categories:
- name: Mathematics/Arithmetic and Number Theory/Number Theory