Micaela Mayero

• Accueil
• Domaines de recherche
  • Présentation
  • Raffinement de réseaux de Petri
  • Projet CerPAN
  • Projet FOST
  • Projet TaMaDi
  • Projet Coquelicot
  • Projet ELFIC
  • Projet MILC
  • Projet LiberAbaci
• Publications
• M2: cours et stages

Contacts:

LIPN - UMR CNRS 7030
Institut Galilée - Université Paris Nord
99 avenue Jean-Baptiste Clément
93430 Villetaneuse
FRANCE

Tél.
Fax
: +33 (0) 1 49 40 36 91
: +33 (0) 1 48 26 07 12
Micaela.Mayero [at] lipn.univ-paris13.fr
Bureau
: A209

Cours de Coq (master M2 PLS, Programmes et preuves)

• Cours 1: Introduction à Coq page par page
  TP0 et TP1


• Cours 2: Coq: des preuves et des nombres page par page
  TP2


• Cours 3: Coq: Ltac, extraction et preuves de programmes (notions) page par page
  TP3

Sujets de stage

• Empilements de Disques & Preuve Formelle


• Real Complexity, Numerical Analysis and Theorem Provers


• Prouveur pédagogique interactif en ligne pour la logique linéaire


• Mesure et Intégrale de Lebesgue en Coq (.pdf)


• Une bibliothèque réelle unifiée pour Coq (.pdf)


• Une extraction en Coq pour les nombres réels et flottants? (.pdf)


• Automatisation de "preuves numériques" en Coq. (.pdf)