coq-trocq.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Enzo Crance <enzo.crance@inria.fr>"
version: "dev"

homepage: "https://github.com/coq-community/trocq"
dev-repo: "git+https://github.com/coq-community/trocq.git"
bug-reports: "https://github.com/coq-community/trocq/issues"
license: "LGPL-3.0-or-later"

synopsis: "A modular parametricity plugin for proof transfer in Coq"
description: """
Trocq is a modular parametricity plugin for Coq. It can be used to
achieve proof transfer by both translating a user goal into another,
related, variant, and computing a proof that proves the corresponding implication.

The plugin features a hierarchy of structures on relations, whose
instances are computed from registered user-defined proof via
parametricity. This hierarchy ranges from structure-less relations
to an original formulation of type equivalence. The resulting
framework generalizes [raw
parametricity](https://arxiv.org/abs/1209.6336), [univalent
parametricity](https://doi.org/10.1145/3429979) and
[CoqEAL](https://github.com/coq-community/coqeal), and includes them
in a unified framework.

The plugin computes a parametricity translation "à la carte", by
performing a fine-grained analysis of the requires properties for a
given proof of relatedness. In particular, it is able to prove
implications without resorting to full-blown type equivalence,
allowing this way to perform proof transfer without necessarily
pulling in the univalence axiom.

The plugin is implemented in Coq-Elpi and the code of the
parametricity translation is fairly close to a pen-and-paper
sequent-style presentation."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.17" & < "8.18"}
  "coq-elpi" {= "dev"}
  "coq-hott" {>= "8.17" & < "8.18~"}
]

tags: [
  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
  "category:Miscellaneous/Coq Extensions"
  "keyword:automation"
  "keyword:elpi"
  "keyword:proof transfer"
  "keyword:isomorphism"
  "keyword:univalence"
  "keyword:parametricity"
  "logpath:Trocq"
]
authors: [
  "Cyril Cohen"
  "Enzo Crance"
  "Assia Mahboubi"
]