Post-Doctoral Research Visit F - M Symmetric Foundations Of Type Theory H/F - 75

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.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