Journée « égalité et terminaison » du 2 février 2010

Venue: La Ciotat (see JFLA 2010)
Programme 13:30 - 18:00:

Pierre-Yves Strub (CoqMT)
Pierre Corbineau (Intégrer l'axiome K de Streicher dans le CIC)
Bruno Barras (Reminder of current termination checking algorithm)
Benjamin Gregoire and Jorge-Luis Sacchini (Type based termination dans Coq)
Andreas Abel (Integration of type based termination with implicit quantification and proof irrelevance)

Compte-rendu sur Cocorico.

Recent news

The Coq team has decided that Coq will be renamed into 'The Rocq Prover'. Background information available here. The rename is currently in preparation, we hope to have a new visual identity and website by the end of 2024, and to do a first release of Rocq around that time.

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).

Check out Discourse and Twitter for recent news.

For recent releases, check out the GitHub repositories of Coq and the Coq Platform.

The Coq Proof Assistant

Journée « égalité et terminaison » du 2 février 2010

Recent news