search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Generate proofs of the correctness of configurations #70

Open tlringer opened 5 years ago

tlringer commented 5 years ago

This corresponds to the optimization of lifting the IP directly being correct. And it may mean that EFF can benefit from our optimization, too, without an excessive amount of work integrating two different lifting algorithms.

Proof for lists and vectors: https://github.com/CoqHott/univalent_parametricity/commit/7dc14e69942e6b3302fadaf5356f9a7e724b0f3c

Use of proof for lists and vectors: https://github.com/CoqHott/univalent_parametricity/commit/b8bab864d1969eccfa4eeeda73f906ce8e1601de

tlringer commented 4 years ago

More generally, this amounts to proving configuration correct

tlringer commented 4 years ago

Of course this requires either ad-hoc or actual univalence