Closed CohenCyril closed 7 months ago
@CohenCyril this project looks very welcome here at a glance, but it would be good to clarify two things:
LGPL-3.0-only
or LGPL-3.0-or-later
?I have my answers now thanks to @ecranceMERCE:
LGPL-3.0-or-later
We will have to figure out together with the Coq-ELPI maintainer how this PR might be handled, but I think that can be a later issue. @CohenCyril feel free to transfer the Trocq repository when you are ready.
@ecranceMERCE you only have the rights to make the transfer.
Thanks everyone, the repo has been transferred: https://github.com/coq-community/trocq
Let's continue the discussion about the project as issues and pull requests to the public repo.
Project name: Trocq - A modular parametricity plugin for proof transfer in Coq
Initial author(s):
Current URL: https://github.com/ecranceMERCE/trocq
Kind: Coq-ELPI plugin / library
License: LGPL-3.0-or-later
Description: Trocq is a prototype of modular parametricity plugin for Coq, aiming to perform proof transfer by translating the goal into an associated goal featuring the target data structures as well as a rich parametricity witness from which a function justifying the goal substitution can be extracted.
The plugin features a hierarchy of parametricity witness types, ranging from structure-less relations to a new formulation of type equivalence, gathering several pre-existing parametricity translations, among which univalent parametricity [1] and CoqEAL [2], under the same framework.
This modular translation performs a fine-grained analysis and generates witnesses that are rich enough to preprocess the goal yet are not always a full-blown type equivalence, allowing to perform proof transfer with the power of univalent parametricity, but trying not to pull in the univalence axiom in cases where it is not required.
The translation is implemented in Coq-Elpi and features transparent and readable code with respect to a sequent-style theoretical presentation.
[1] The marriage of univalence and parametricity, Tabareau et al. (2021) [2] https://github.com/coq-community/coqeal
Status: Actively maintained
New maintainer: The initial authors should be maintainers