Coquelicot

We hired Catherine Lelay as INRIA Saclay - Île-de-France PhD student in October 2011.

Meetings

• 09/09/2011: Kick-off meeting in Orsay
• 11/22/2011: Special day about classic realisability in Orsay
  Technical program:
  10h: Guillaume Melquiond;
  Les réels standards de Coq : pourquoi les garder, pourquoi les jeter
  10h15: Micaela Mayero;
  Histoire des réels dans les TP et tentative de fusion entre Reals et CoRN
  10h45: Alexandre Miquel;
  Enjeux de la réalisabilité pour l'extraction de programme en logique intuitionniste et en logique classique
  11h45: Pause déjeuner
  13h: Alexandre Miquel;
  L'extraction classique en Coq
  14h: Cyril Cohen;
  Une formalisation des nombres algébriques réels à partir de réels constructifs, en Coq
  14h30: Lionel Rieg;
  Les problèmes soulevés par des réels classiquement réalisables dans Coq
  15h: Discussions
• 09/10/2012: meeting in Orsay
• 09/20/2013: meeting in Palaiseau (with also A. Barillec, F. Chyzak, L. Rieg).
  Slides presenting Coquelicot.
• many Orsay meetings