meta.yml

fullname: Paramcoq
shortname: paramcoq
organization: coq-community
community: true
action: true
synopsis: Plugin for generating parametricity statements to perform refinement proofs
description: >
  The plugin is still in an experimental state. It is not very user
  friendly (lack of good error messages) and still contains bugs. But
  is useable enough to "translate" a large chunk of standard library.
doi: 10.4230/LIPIcs.CSL.2012.399
publications:
  - pub_title: Parametricity in an Impredicative Sort
    pub_url: https://hal.archives-ouvertes.fr/hal-00730913/
    pub_doi: 10.4230/LIPIcs.CSL.2012.399
authors:
  - name: Chantal Keller
    initial: true
  - name: Marc Lasson
    initial: true
  - name: Abhishek Anand
  - name: Pierre Roux
  - name: Emilio Jesús Gallego Arias
  - name: Cyril Cohen
  - name: Matthieu Sozeau
maintainers:
  - name: Pierre Roux
    nickname: proux01
license:
  fullname: MIT
  identifier: MIT
supported_coq_versions:
  text: >
    The master branch tracks the development version of Coq, see
    releases for compatibility with released versions of Coq.
  opam: '{= "dev" }'
plugin: true
categories:
  - name: 'Miscellaneous/Coq Extensions'
keywords:
  - name: paramcoq
  - name: parametricity
  - name: ocaml module
namespace: Param
opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'
tested_coq_opam_versions:
  - version: 'dev'
documentation: |
  Available commands
  ------------------

  The default arity is 2.

  - Parametricity *ident* as *name* [arity *n*].

  Declare the translation named *name* from the translation of the constant or inductive *ident*.

  - Parametricity [Recursive] *ident* [arity *n*] [qualified].

  The default name for the translation of the constant or inductive *ident* is automatically generated (from its unqualified name).
  You can use the `Recursive` option to recursively translate all the constants and inductives which are used by *ident*.
  You can use the `qualified` option to use a qualified default name for the translated constants and inductives. The default name then has the form `Module_o_Submodule_o_ident` if *ident* lies in the `Module.Submodule` namespace.

  - Parametricity Translation *term* [as *name*] [arity *n*].

  Define a new constant named *name* obtained by computing the parametricity translation of *term*.

  - Parametricity Module *modulepath*.

  Recursively translate everything in a module.

  - Realizer *constant or variable* [as *name*] [arity *n*] := *term*.

  Declare *term* to be the translation of a constant.
  Useful to translate terms containing section variables, or axioms.

  Note that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import `ProofIrrelevence`).

  - [Global | Local] Parametricity Tactic := t.

  Use the tactic t to solve proof obligations generated by the `Parametricity` command.