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

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.

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

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;

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

Languages: proof assistants (Rocq, Lean, Agda, Isabelle, ...)

• 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