Post-Doctoral Research Visit F - M Symmetric Foundations Of Type Theory H/F INRIA
Paris - 75 CDD- 12 mois
- Bac +2
- Bac +3, Bac +4
- Bac +5
- Service public des collectivités territoriales
Les missions du poste
Post-Doctoral Research Visit F/M Symmetric foundations of type theory
Le descriptif de l'offre ci-dessous est en Anglais
Type de contrat : CDD
Contrat renouvelable : Oui
Niveau de diplôme exigé : Thèse ou équivalent
Fonction : Post-Doctorant
Contexte et atouts du poste
The job is within the framework of the Malinca project (http://malinca.org). IT will BE located at the IRIF lab in Paris.
Travel expenses are covered within the limits of the scale in force.
Mission confiée
Dependent type theory, which is at the heart of several proof assistants, such as Agda, Lean, Rocq, is traditionally based on the "natural deduction" formalism, equipped with universes and dependent elimination of positive connectives. In the absence of those last two features, IT is known that natural deduction is only one formal approach among others, besides e.g. sequent calculus and axiomatic systems. Among these last two approaches, sequent calculus has the particularity to spontaneously exhibit symmetries.
There is a three-way "Curry-Howard-Lambek" correspondence between proofs of natural deduction, programs of lambda-calculus and morphisms of cartesian closed categories. On its side, the symmetry of sequent calculus echo the value/stack symmetry of abstract machines in programming. An associated three-way correspondence with category theory is currently emerging, adding the symmetry of adjunctions to the picture.
The symmetry of sequent calculus directly leads to a smooth integration of classical logic into the realm of computation. Classical logic features are also at work in choice axioms : a standard way to express the axiom of choice in type theory is as a commutation of quantification with propositional truncation, which directly relates to the subclassical "double negation shift" principle.
The objective of the post-doc is to explore how to combine the above observations into a more general picture. In particular, IT intends :
- To clarify the emerging three-way Curry-Howard-Lambek-style correspondence between sequent calculus, abstract machines and adjunctions
- To explore type theory in forms different than natural deduction, namely sequent calculus or axiomatic style, paving the way to more symmetries between hypotheses and conclusions in the presentation of type theory and a tighter connection to category theory
- To eventually add classical logic as a dualisation principle and choice principles as shift principles to the picture
- To explore the impact of the results on the design of type-theoretic proof assistants
Compétences
Expertise expected in type theory, structural proof theory and category theory.
Familiarity with the question of computing with the axiom of choice welcomed.
Familiarity with proof assistants also welcomed.
Fluency in French or English recommended.
Avantages
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave : 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
Bienvenue chez INRIA
A propos d'Inria
Inria est l'institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l'interface d'autres disciplines. L'institut fait appel à de nombreux talents dans plus d'une quarantaine de métiers différents. 900 personnels d'appui à la recherche et à l'innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'eorce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.
Hellowork a estimé le salaire pour ce métier à Paris
Le recruteur n'a pas communiqué le salaire de cette offre mais Hellowork vous propose une estimation (fourchette variable selon l'expérience).
Estimation basée sur les données INSEE et les offres d’emploi similaires.
Estimation basse
42 500 € / an 3 542 € / mois 23,35 € / heureSalaire brut estimé
50 000 € / an 4 167 € / mois 27,47 € / heureEstimation haute
62 500 € / an 5 208 € / mois 34,34 € / heureCette information vous semble-t-elle utile ?
Merci pour votre retour !
- Paris - 75
- CDD
Créez une alerte
Pour être informé rapidement des nouvelles offres, merci de préciser les critères :
Finalisez votre candidature
sur le site du recruteur
Créez votre compte pour postuler
sur le site du recruteur !
sur le site du recruteur
sur le site du recruteur !
Ces offres pourraient aussi
vous intéresser
Recherches similaires
- Job Ingénieur en informatique industrielle
- Job Industrie
- Job Technicien de maintenance industrielle
- Job Peintre industriel
- Job Mécanicien industriel
- Job Préparateur méthode
- Job Conseiller technique
- Entreprises Industrie
- Entreprises Ingénieur en informatique industrielle
- Entreprises Paris
- Job Fonction publique
- Job Collectivités
- Job Fonction publique territoriale
- Job Public
- Job Numérique
- Job Anglais Paris
- Job Fonction publique Paris
- Job Cdd Paris
- Job Collectivités Paris
- Job Fonction publique territoriale Paris
- INRIA Paris
- INRIA Ingénieur en informatique industrielle
{{title}}
{{message}}
{{linkLabel}}