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

Descrizione

Testo originale dell'annuncio (in inglese)

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;