Pôle "Interfaces et Environnements"

Environnement de développement de preuves

CtCoq: interface graphique pour le système de preuve Coq

manipulation directe pour la conduite de la preuve

mécanisme d'explication textuelle des preuves

raisonnements sur des spécifications sémantiques