Sujets de Stages 2008-2009

proposées par l'Equipe-Projet Typical

• Nombres Algébriques en Coq; proposé par Assia Mahboubi
• Généralisation des techniques SMT au formules de Harrop. Proposé par Stéphane Lengrand, Germain Faure et Assia Mahboubi (contactez-les).
• (Super)-développements finis généralisés et filtrage d'ordre supérieur. Proposé par Germain Faure (contactez-le).
• Normalisation forte de théories complexes avec des Lambda-sets. Pour fanas de réductibilité seulement; contacter Benjamin Werner pour les détails.
• Importation de preuves HOL en Coq par Benjamin Werner.

Par des équipes apparentées

• Automatisation de preuves numériques par Micaela Mayero au LIPN.
• La page des stages du projet Proval (INRIA et Orsay).