Skip to content

Commit

Permalink
fix link to univalent parametricity
Browse files Browse the repository at this point in the history
  • Loading branch information
chenson2018 committed Aug 1, 2024
1 parent d417b00 commit fa7db50
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ 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://arxiv.org/abs/1209.6336) and
[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
Expand Down

0 comments on commit fa7db50

Please sign in to comment.