STAGE Mesure et Intégrale de Lebesgue en Coq

Date de mise à jour de l’offre

Ets public nation scientifique :

Laboratoire d'Informatique de Paris Nord (sujet de stage dans le cadre du projet DIM-RFSI 2018 MILC, soutenu par la région Ile de France)

Description de la mission

La méthode des éléments finis (MEF) pour la résolution numérique d'équations aux dérivées partielles est au cœur de nombreux programmes de simulation dans l'industrie. Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Il s'agit de poser les fondements qui permettront de prouver la correction d'une bibliothèque implantant la MEF. Ces preuves reposent entre autres sur la théorie de la mesure, l'intégrale de Lebesgue, les distributions et les espaces de Sobolev. Ce stage a pour but de prouver formellement en Coq un certain nombre de résultats mathématiques bien connus tels que la construction de l'espace fonctionnel L^2 ainsi que les propriétés afférentes, en particulier la complétude pour la norme associée au produit scalaire. Ce n'est évidemment pas seulement une «traduction» de livres de
mathématiques vers un assistant de preuves. Cela nécessitera de bien comprendre les preuves existantes de façon à les factoriser, les simplifier voire à les généraliser. Il faudra également choisir les bonnes formalisations pour simplifier les preuves ultérieures. (https://www-lipn.univ-paris13.fr/~mayero/stageM2_milc.pdf)

Profil recherché

Avoir des connaissances dans le domaine des preuves formelles: logique, Coq (ou autre)

Niveau de qualification requis

Bac + 4/5 et +
  • Employeur
    Ets public nation scientifique
  • Secteur d’activité de la structure
    Enseignement - Formation - Recherche
  • Effectif de la structure
    Plus de 250 salariés
  • Site internet de la structure
    https://lipn.univ-paris13.fr
  • Type de stage ou contrat
    Stage pour lycéens et étudiants en formation initiale
  • Date prévisionnelle de démarrage
  • Durée du stage ou contrat
    Plus de 2 mois et jusqu'à 4 mois
  • Le stage est-il rémunéré ?
    Oui
  • Niveau de qualification requis

    Bac + 4/5 et +
  • Lieu du stage
    LIPN- Institut Galilée
    99 av J.-B. Clément
    93430 VILLETANEUSE
  • Accès et transports
    ligne H depuis Gare du Nord ou Tram T8 ou T11