researchJobsDoctorate in Fundamental Mathematics and Computer Science (m/f)
Doctorat en mathématiques et informatique fondamentale (H/F) — Machine-translated title
From the ad
Description of the post
Subject of Thesis
Linear duality and higher algebraic effects in homotopic type theory
The objective of this thesis will be to define a unified, syntactic and functional framework, which integrates linear logic, algebraic effects, and homotopic type theory. This will be done from the semantic interpretation of a system of dependent types with universe Type: Type given in the language of domain theory. First, the structures and properties of this interpretation will be axiomatized, and the relationship to the relational model of linear logic will be established. Extensions of the theory of dependent types with intersection types will then be formulated, relying on the correspondence between intersection types and finite elements of relational semantics. In parallel, the links between linear continuations, duality in dialogue games and higher algebraic effects will be studied within the framework of a theory of homotopic and multimodal types.
Competences:
• Good knowledge of the theory and semantics of dependent types with equality
• Good knowledge of a proof assistant such as Agda, Isabelle, Lean or Rocq on the formalization and internal implementation aspects
• Good knowledge of one or more programming and specification languages such as Haskell, OCaml, Rust
• English: B2 (European Reference Framework)
• Conceptualization capability
• Critical sense
• Sense of organization
• Ability to work as a team
Your Working Environment
The project aims to contribute to the development of a new generation of proof assistants, who integrate into their cores a linguistic layer and automated assistance tools to guide the scientist and facilitate the construction of certified mathematical documents, from the choice of concepts and definitions to the development of theorems and demonstrations.
Constraints and risks
None
Remuneration and benefits
Remuneration
The remuneration is a minimum of 2300,00 € monthly
Annual leave and TWU
44 days
Practice and compensation of TT
TT practice and compensation
Transport
Support at 75% cost and sustainable mobility package up to 300€
About the offer
Supply Reference UMR8243-LAUPIN-004 Section(s) CN / Research Area Computer science: basics of computing, calculations, algorithms, representations, operationsAbout CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. His unique position as a multi-specialist allows him to associate the different disciplines in order to face the most important challenges of the contemporary world, in connection with the actors of change.
The CNRS
Research occupations
Machine translation (OPUS-MT) — the original text is authoritative
Show the original advertisement
Description du Poste
Sujet De Thèse
Dualité linéaire et effets algébriques supérieurs en théorie des types homotopiques
L’objectif de cette thèse sera de définir un cadre unifié, syntaxique et fonctoriel, qui intègre logique linéaire, effets algébriques, et théorie des types homotopiques. On partira pour cela de l’interprétation sémantique d’un système de types dépendants avec univers Type : Type donné dans le langage de la théorie des domaines. Il s’agira tout d’abord d’axiomatiser les structures et propriétés de cette interprétation, et de dégager le lien avec le modèle relationnel de la logique linéaire. On formulera ensuite des extensions de la théorie des types dépendants avec types intersection, en s’appuyant sur la correspondance entre types intersections et éléments finis de la sémantique relationnelle. En parallèle, on étudiera les liens entre continuations linéaires, dualité dans les jeux de dialogue et effets algébriques supérieurs, dans le cadre d'une théorie des types homotopique et multimodale.
Compétences:
• Bonne connaissance de la théorie et de la sémantique des types dépendants avec égalité
• Bonne connaissance d’un assistant de preuve tel que Agda, Isabelle, Lean ou Rocq sur les aspects formalisation et implémentation interne
• Bonne connaissance d’un ou plusieurs langages de programmation et de spécification tels que Haskell, OCaml, Rust
• Anglais : B2 (Cadre européen de référence)
• Capacité de conceptualisation
• Sens critique
• Sens de l'organisation
• Aptitude au travail en équipe
Votre Environnement de Travail
Le projet a pour objectif de participer au développement d’une nouvelle génération d’assistants à la preuve, qui intègrent dans leurs noyaux une couche linguistique et des outils d'assistance automatisée pour guider le scientifique et faciliter la construction de documents mathématiques certifiés, depuis le choix des concepts et des définitions, jusqu’à l'élaboration des théorèmes et des démonstrations.
Contraintes et risques
Aucuns
Rémunération et avantages
Rémunération
La rémunération est d'un minimum de 2300,00 € mensuel
Congés et RTT annuels
44 jours
Pratique et Indemnisation du TT
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
À propos de l’offre
Référence de l’offre UMR8243-LAUPIN-004 Section(s) CN / Domaine de recherche Sciences informatiques : fondements de l'informatique, calculs, algorithmes, représentations, exploitationsÀ propos du CNRS
Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.
Le CNRS
Les métiers de la recherche
Advertisement text from CNRS, no licence stated; reproduced with attribution.
The employer's ad is the binding version. Apply through their system.
?
Saved calls and ads appear on your calendar, and their deadlines are included when you export it. Nothing else is added for you.