Stream: CUDW 2020

Topic: WG: Contravariant subtyping


view this post on Zulip Kenji Maillard (Dec 01 2020 at 13:12):

@Hugo Herbelin would you have some time to discuss about your cep on (re-)adding contravariant subtyping to coq ? We are working on close topics with @Théo Laurent and would be interested to learn more.

view this post on Zulip Hugo Herbelin (Dec 01 2020 at 14:59):

We can talk after Matthieu's talk?? (I'll be free up to 5pm)

view this post on Zulip Kenji Maillard (Dec 01 2020 at 15:22):

@Hugo Herbelin let's do that. Room 2 ?
@Matthieu Sozeau Would you like to join to explain the metacoq side of the story ?

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 15:23):

Sure, after Michael's talk though

view this post on Zulip Kenji Maillard (Dec 02 2020 at 13:32):

@Hugo Herbelin @Matthieu Sozeau Are you around to finish this discussion ?

view this post on Zulip Hugo Herbelin (Dec 02 2020 at 13:38):

Which room?

view this post on Zulip Kenji Maillard (Dec 02 2020 at 13:41):

room 2 is empty

view this post on Zulip Bas Spitters (Dec 02 2020 at 13:49):

We're interested in eta-conversion (in relation to metacoq) too for our work on dearging.
https://www.cs.au.dk/~spitters/Concert2.pdf


Last updated: Oct 16 2021 at 07:02 UTC