@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.
We can talk after Matthieu's talk?? (I'll be free up to 5pm)
@Hugo Herbelin let's do that. Room 2 ?
@Matthieu Sozeau Would you like to join to explain the metacoq side of the story ?
Sure, after Michael's talk though
@Hugo Herbelin @Matthieu Sozeau Are you around to finish this discussion ?
room 2 is empty
We're interested in eta-conversion (in relation to metacoq) too for our work on dearging.
Last updated: Oct 16 2021 at 07:02 UTC