Contexte et atouts du poste
The job is within the framework of the Malinca project and in particular on consolidating the logical foundations of mathematical proof assistants ( 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
Emerged from the correspondence between proofs and programs, dependent type theory is a formalism which has proved its worth as a foundation of mathematics, as witnessed by the success of several proof assistants relying on it, such as Agda, Lean, Rocq, and, to some extent, Isabelle.
Originally confined to intuitionistic logic and functional programming, the articulation between dependent type theory, imperative programming (control operators, memory assignment, exceptions, ...), classical axioms (excluded-middle, axiom of choice, extensionality), logical translations (double-negation, forcing, ...) has made a lot of progresses in the recent years.
Further connections with algebra and geometry (category theory, homotopy theory, topos theory, sheaf theory, ...) have also emerged.
In this context, the objective of the postdoc will be to study more finely the articulation between intuitionistic and classical variants of the axiom of choice (bar induction, unique choice, ...).
Recursive translations as well as model constructions could be considered, studying the compatibility and incompatibility of combinations of axioms, with a focus in particular on the combination of classical logic and unique choice or on the extraction of bar induction trees.
Compétences
Expertise expected in type theory, programming languages, machine-checked proofs, and, in particular, in the proof-theoretical properties of various formulations of the axiom of choice.
Fluency in French or English recommended.
Avantages