RESPONSABILITÉS : Ref Emploi : LAMAGULI2 Affectation : Laboratoire de Mathématiques (composante d'affectation : UFR SceM) - Campus du 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. Plus d'information sur le projet GULI à consulter sur notre site internet ICI 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 PROFIL RECHERCHÉ : I. Conditions d'exercice A temps plein au LAMA (bureau sur place). Déplacements prévus au LAPP à Annecy. Le post-doctorant ou la post-doctorante aura accès aux infrastructures de l'USMB. 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. 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