Template Coq Day July 4th

We will have a meeting about all things Template Coq on July 4th at Inria Paris in room C119 Ada Lovelace. Expect a few informal presentations of ongoing work in the morning and an afternoon "hackaton". One goal could be to converge on the most common interfaces / features of the monad for all uses and to be able to make a minimal 8.8 release for people to build on.

Schedule

• 9.30: Welcome
• 10: M. Sozeau: checker and proving proof erasure for CertiCoq
• 10.25: A. Guéneau and J.H. Jourdan: universe constraint checking
• 10.50: T. Winterhalter: ETT to ITT to (Template)Coq
• 11.15: Break
• 11.45: C. Mangin: positivity and guard condition
• 12.10: S. Boulier: translations (e.g. parametricity)
• 12.35: Y. Forster: Extraction to cbv lambda-calculus
• 13: Lunch, at le Repaire
• Afternoon: open discussion/hackaton

At 7pm, there is the first Coq Meetup happening at Mines ParisTech:

https://www.meetup.com/fr-FR/Coq-Users-in-PariS/events/251951527/

Participants (especially for non-Inria-Paris people, I'll have to send a list)

• Matthieu Sozeau
• Théo Winterhalter
• Cyprien Mangin
• Nicolas Tabareau
• Simon Boulier
• Yannick Forster
• Maxime Dénès
• Armaël Guéneau
• Jacques-Henry Jourdan
• Eric Tanter
• Vadim Zaliva