Développement

• Generation d'infrastructure pour les indices de De Bruijn en Coq.

• Implantation d'un module d'environnements génériques en Coq.

• LoopW : certification de programmes impératifs et logique classique du premier ordre.

Autres :

• MotsCroises est un générateur de grilles de mots-croisés à vocation pédagogique.