ADT Coq

L'action de développement technologique (ADT) Coq regroupe les personnes et équipes participant collectivement à l'implantation du logiciel d'aide à la preuve Coq.

Les équipes concernées par l'action sont les équipes INRIA TypiCal, ProVal et Marelle, π r², ainsi que l'équipe CPR du CNAM. Il est aussi prévu que l'ADT fonctionne en partenariat avec l'équipe Formes du LIAMA.

L'INRIA met à la disposition de l'ADT Coq un ingénieur localisé à Sophia-Antipolis et ayant pour tâche la mise en place d'une communication structurée entre Coq et des outils externes et un ingénieur localisé sur la région parisienne et ayant pour tâche l'extension de l'interface graphique CoqIDE.

L'ADT Coq est coordonnée par Hugo Herbelin.

Le document décrivant le projet.

La réunion de démarrage du 29 octobre 2008.

La journée « bibliothèques » du 11 décembre 2008 à Sophia-Antipolis.

La journée « automatisation » du 24 mars 2009 à Paris.

La journée « tactiques » du 30 juin 2009 à Palaiseau.

La journée « égalité et terminaison » du 2 février 2010 à La Ciotat.

La journée « interfaces » du 27 octobre 2010 à Paris.

Le premier workshop Coq (soutenu par l'ADT) a eu lieu le 21 août 2009 à Munich en marge de TPHOLs.

Le second workshop Coq (soutenu par l'ADT) a eu lieu le 9 juillet 2010 à Édimbourg en marge de ITP (FLoC).

L'ADT a soutenu en 2009 et 2010 l'école d'été Asie-Pacifique sur les méthodes formelles.