PhD Position F/M A study of forcing and second-order abstract syntax in type theory

Contexte et atouts du poste

The candidate will be cosupervised by Hugo Herbelin in Paris and Ambrus Kaposi in Budapest.

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

Mission confiée

The objective of the PhD is to study, design and implement variants of type theory with native support for second-order binder and modalities.

Principales activités

The PhD is in collaboration between Paris and Budapest with stays alternating in both locations. 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, ...)

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