Coq Call 2021 06 30
- June 30th 2021, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- (more or less) recent progress on small inversions. I (Jean-François Monin) will show better techniques than the one presented at Coq WS 2010 and ITP13 : a version which is simpler to write and suits many practical needs, and a less easy one which is needed in combination with the guard condition of recursive programs. Both versions are able to deal with cases which seem out of reach of Coq standard inversion.
Slides at http://www-verimag.imag.fr/~monin/Talks/sir.pdf
Differences:
- slide 2 replaced with references to code and last paper on the Braga method
- slide 34 added (useful for dependent data types)
Coq scripts : http://www-verimag.imag.fr/~monin/Proof/Small_inversions/2021/
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.