CRGTCoq20130214

Pierre Letouzey edited this page Oct 18, 2017 · 6 revisions

A Coq working group took place on february 14th 2013 at Paris 7 University. About 20 persons participated and it consisted of the following presentations:

  • Enrico Tassi: Adding a positive/negative cache to the term comparison routine GTCoq2013_tassi.pdf (lost attachment)

  • Maxime Dénès: A native compiler for Coq: current status, perspectives and discussion GTCoq2013_denes.pdf (lost attachment)

  • François Ripault: Introducing the new coqdoc GTCoq2013_ripault.pdf (lost attachment)

  • Micaela Mayero: Experimentations sur les réels de Coq GTCoq2013_mayero.pdf (lost attachment)

  • Pierre-Nicolas Tollitte: Extraction de code à partir de spécifications inductives.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.