Avec plus de 15 000 étudiants, une offre de formation pluridisciplinaire riche d’une centaine de diplômes nationaux et des laboratoires de qualité qui la font apparaître dans le classement de Shanghai, l'Université Savoie Mont Blanc, membre de l’alliance européenne UNITA, est un établissement à taille humaine qui conjugue la recherche et la professionnalisation, la proximité avec ses territoires et une large ouverture sur le monde. Sur ses trois campus d’Annecy, du Bourget-du-Lac et de Jacob-Bellecombette (Chambéry), elle propose différents cursus courts et longs (Diplômes d’université, Bachelors universitaires de technologie, Licences, Masters, Doctorats, Diplômes d'ingénieurs) que ce soit en formation initiale ou continue, en alternance ou via diverses validations, en présentiel ou à distance.
Le Laboratoire de Mathématiques (LAMA) est une unité mixte de recherche CNRS / Université Savoie Mont Blanc, situé sur le campus scientifique du Bourget-du-Lac en Savoie.
Il est organisé autour de trois équipes de recherche : EDPs2 (Equations aux Dérivées Partielles : Etudes Déterministes et Probabilistes), Géométrie, et LIMD (Logique, Informatique et Mathématiques Discrète). Cette diversité de thèmes de recherche dans un seul laboratoire est l'expression de l'unité des mathématiques dans ses trois composantes : mathématiques pures, mathématiques appliquées et informatique mathématique. Le dénominateur commun est d'une part, la qualité de la recherche fondamentale, et, d'autre part, le souci des applications. Il s'agit en effet des applications dans d'autres sciences (géophysique, physique, biologie, mécanique et informatique) ou dans d'autres domaines des mathématiques (géométrie appliquée en théorie du contrôle…) ou encore dans le domaine de la pédagogie.
Ref Emploi : LAMAGULI2
Affectation : Laboratoire de Mathématiques (composante d’affectation : UFR Sciences et Montagne) - Campus scientifique - 73376 Le Bourget-du-Lac
I. Description du projet et activités de recherche associées
La plupart des codes de simulation numérique et d’analyse de données en modélisation effectuent leurs calculs sans vérification de cohérence dimensionnelle. Ainsi, ajouter une longueur en mètres à une force en Newton ne sera pas, dans la majorité des cas, détecté comme une erreur. Or les systèmes de typage servent justement en principe à détecter des erreurs de nature similaire en interdisant par exemple l’addition de valeurs numériques à des tableaux de nombres. Pourtant, malgré l’existence de bibliothèques informatiques de gestion des unités exploitant les systèmes de typage, peu sont utilisées tellement elles sont éloignées des cas d’application concrets des physicien·nes. Les solutions proposées jusqu’à présent par les théoricien·nes des langages de programmation ont eu tendance soit à se concentrer sur les cas les plus conceptuellement simples, soit à aborder les cas délicats comme autant de problèmes indépendants conduisant à des solutions trop complexes pour être mises en pratique. Plus fondamentalement, c’est même le concept de système de grandeurs et d’unités qui semble manquer de formalisation mathématique.
Le projet GULI (Grandeurs et Unités pour les Langages Informatiques) vise à étudier cette question sous un nouvel angle mêlant théories des catégories, théorie des types, langages de programmation, preuve formelle, physique numérique et implémentation. Au-delà du cas d’application des unités, l’objectif plus large est de démontrer la pertinence d’approches interdisciplinaires mêlant mathématiques et informatique théorique pour la vérification de simulations physiques. Dans ce cadre, l’équipe, qui réunit un astrophysicien numéricien, Vincent Reverdy (LAPP – Laboratoire d’Annecy de Physique des Particules), et deux théoriciens des langages de programmation, Tom Hirschowitz et Pierre Hyvernat (LAMA – Laboratoire de Mathématiques de l’Université Savoie Mont Blanc) propose cette offre de contrat post-doctoral de 18 mois afin de tenter d’élaborer, ensemble, une solution conceptuellement claire couvrant tous les cas d’application.
II. Missions et activités du poste
La personne recrutée sera intégrée dans l’équipe Logique Informatique Mathématiques Discrètes du Laboratoire de Mathématiques de l’Université Savoie Mont Blanc. Elle participera à la recherche d’une méthode d’intégration des systèmes d’unités au sein des langages de programmation. La nature du travail de recherche mêlera des aspects théoriques (théorie des catégories, théorie des types...) à des aspects pratiques (prototypage, preuve formelle...) et impliquera des allers-retours réguliers entre les deux. Suivant les préférences de la personne recrutée, le prototypage pourra être effectué au travers d’une approche « deep embedding » dans un assistant de preuve (Coq/Rocq, Agda,…), ou bien dans un langage de programmation généraliste. Au sein de ce cadre interdisciplinaire combinant réflexion théorique et implémentation, il sera possible de mettre davantage l’accent sur certains aspects du projet suivant les intérêts de la personne sélectionnée.
Pour tout renseignement complémentaire et contact utiles, veuillez consulter l'offre en cliquant ICI
I. Conditions d’exercice
A temps plein au LAMA (bureau sur place). Déplacements prévus au LAPP à Annecy.
Personnel de l’université, le post-doctorant ou la post-doctorante aura accès aux infrastructures de l’USMB (bibliothèques, activités du service des sports, etc.). Le LAMA dispose d’une bibliothèque, d’une salle de séminaire, d’une salle de convivialité, d’une douche et d’un local à vélos sécurisé. Le lac du Bourget se situe à moins de 2km du laboratoire. Le campus est accessible depuis Chambéry ou Aix-les-Bains en transports en commun, en vélo (piste cyclable), et/ou en voiture/co-voiturage.
II. Spécificités liées au poste
Il s’agit d’un poste dans le cadre d’un projet interdisciplinaire impliquant deux laboratoires : l’un de mathématiques/informatique, l’autre de physique. Scientifiquement, le post-doctorant ou la post-doctorante sera en conséquence amené·e à interagir avec des personnes d’horizons disciplinaires différents. En termes logistiques, le post-doctorant ou la post-doctorante sera accueilli·e au laboratoire de Mathématiques au Bourget-du-Lac, avec T. Hirschowitz et P. Hyvernat. V. Reverdy étant basé au LAPP à Annecy, des réunions régulières seront organisées pour faciliter les interactions.
III. Compétences attendues
Pour ce poste, il est nécessaire de posséder des compétences sur le typage des langages de programmation, à la fois théoriques et pratiques. Par exemple, des compétences dans un ou plusieurs des domaines suivants seraient pertinentes : assistants de preuve (Coq/Rocq, Agda, Lean...), théorie des types, inférence de types… Des connaissances en théorie des catégories seraient un avantage significatif. Un intérêt pour l’interdisciplinarité est un plus.
IV. Conditions de recrutement
Le recrutement est ouvert aux personnes titulaires d’un doctorat délivré par une université française, ou d’un diplôme reconnu équivalent par l’université, notamment un doctorat ou PhD délivré par une université étrangère.
Il s’agit d’un contrat de niveau A à durée déterminée à temps plein pour une durée de 18 mois avec une prise de poste flexible à l’automne 2025. Une date de début indicative est donnée au 01/10/2025 avec une fin de contrat au 31/03/2027.
Les deux premiers mois du contrat seront considérés comme période d’essai.
Rémunération brute mensuelle pour le temps plein proposé à partir de 2 638,61 euros (échelon 2 à la grille de rémunération des maîtres de conférences de classe normale au 1er janvier 2024) et jusqu’à 3 189,96 euros (échelon 4) - fourchette de rémunération proposée pour tenir compte de l’expérience professionnelle.
V. Comment candidater
Transmettre les documents suivants dans un fichier pdf unique nommé GULI2_NOM PRENOM :
Curriculum Vitae
Lettre de motivation
Copie(s) du ou des diplômes
Rapport de soutenance de thèse