PhD Position F/M Study and formalisation of algebraic structures hierarchies in proof assistants

Contexte et atouts du poste

The candidate will be a member of the IMJ-PRG lab, a member of the Picube team at the IRIF lab, and a member of the Malinca project.

Travel expenses will be covered within the limits of the scale in force.

Mission confiée

The recruited person will prepare their PhD under the direction of Riccardo Brasca (IMG-PRJ) in cosupervision with Hugo Herbelin and Sarah Reboullet (IRIF).

The objective of the PhD is to study, design and implement algebraic structures hierarchies in proof assistants. It will include:

• an empirical analysis of the use of algebraic structures hierarchies in Mathlib (Lean) and Mathcomp (Rocq), as well as in other systems;
• the design and study of algebraic structures hierarchies, ensuring properties by construction and possibly supporting reasoning modulo representation;
• implementation of algebraic structures hierarchies.

Principales activités

The PhD work will notably consist in:

• bibliography work;
• (possibly) attend some additional graduate courses to complement the curriculum;
• regular working sessions with the supervisors;
• contribute to the scientific life of the lab (seminar, working groups and lab meetings, ...);
• writing of reports and publications, presentation at seminars and conferences;
• possibly, teaching assistantship;
• possibly participate to a young research school during the course of the PhD;
• writing of the thesis manuscript and defense of the thesis.

Compétences

Technical skills and level required : master in mathematics or theoretical computer science

Languages : proof assistants (Rocq, Lean, Agda, Isabelle, ...), functional programming (OCaml, Haskell, ...)

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