Stream: Coq devs & plugin devs

Topic: Reverse coercions


view this post on Zulip Cyril Cohen (Apr 12 2021 at 12:02):

@Matthieu Sozeau @Arthur Charguéraud should we open a working group on the topic?

view this post on Zulip Enrico Tassi (Apr 12 2021 at 12:15):

As I wrote on discourse, this reminds me of this paper https://arxiv.org/abs/1103.3320 which is using Matita's coercion system to insert Pant as a cast, and resolve the resulting unification problem via CS.

view this post on Zulip Arthur Charguéraud (Apr 12 2021 at 12:16):

I'm happy to contribute on the design and the testing of this proposal.

view this post on Zulip Matthieu Sozeau (Apr 12 2021 at 12:35):

Yes

view this post on Zulip Ali Caglayan (Jun 01 2021 at 11:30):

I am also interested in something like this


Last updated: Oct 21 2021 at 20:02 UTC