Kenji Maillard (Dec 01 2020 at 13:12): 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.
Hugo Herbelin (Dec 01 2020 at 14:59):We can talk after Matthieu's talk?? (I'll be free up to 5pm)
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 ?
Matthieu Sozeau (Dec 01 2020 at 15:23):Sure, after Michael's talk though
Kenji Maillard (Dec 02 2020 at 13:32):@Hugo Herbelin @Matthieu Sozeau Are you around to finish this discussion ?
Hugo Herbelin (Dec 02 2020 at 13:38):Which room?
Kenji Maillard (Dec 02 2020 at 13:41):room 2 is empty
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: Jun 10 2023 at 23:01 UTC