CRGTCoq20130214 - coq/coq GitHub Wiki

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.

To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.

CC0

By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.

⚠️ **GitHub.com Fallback** ⚠️