[TYPES/announce] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary)

[Ambrus Kaposi]

Dear all,

I have two postdoc positions available in Budapest on Higher
Observational Type Theory funded by the HOTT ERC project. The starting
point of the project is a theory of internal parametricity [1] which
supports a baby identity type which is reflexive and a congruence, but
not symmetric or transitive. The goal is to extend this to a proper
identity type supporting transport. See also [2,3,4].

The project starts on 1 May 2025 and is 5 years long. Later starting
dates and shorter lengths are possible. The salary will be between
4,600--5,100 EUR/month gross (but in Hungarian forints) depending on
work experience and administrative factors (institutional and project
remuneration rules, legal environment). Involvement in teaching
computer science students is encouraged. There is a generous budget
for travel available. The place of work is the type theory research
group [5] at the Faculty of Informatics [6] at Eötvös Loránd
University in Budapest.

If you are interested, please get in touch with me.

Best wishes,
Ambrus

akaposi at inf.elte.hu
https://urldefense.com/v3/__https://akaposi.web.elte.hu__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYzSe-hXLg$ 




[1] Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael
Shulman: Internal Parametricity, without an Interval. Proc. ACM
Program. Lang. 8(POPL): 2340-2369
(2024). https://urldefense.com/v3/__https://doi.org/10.1145/3632920__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYxyBc6fWQ$ 

[2] Michael Shulman. Towards a Third-Generation HOTT (Parts
1--3). Homotopy Type Theory Seminar at Carnegie Melon
University. Spring 2022. Slides:
https://urldefense.com/v3/__https://home.sandiego.edu/*shulman/papers/hott-cmu-day1.pdf__;fg!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYwfR7mH7A$ 
https://urldefense.com/v3/__https://home.sandiego.edu/*shulman/papers/hott-cmu-day2.pdf__;fg!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYxk-DyTHQ$ 
https://urldefense.com/v3/__https://home.sandiego.edu/*shulman/papers/hott-cmu-day3.pdf__;fg!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYxgdy-ODQ$ 
Videos:
https://urldefense.com/v3/__https://www.youtube.com/watch?v=FrxkVzItMzA__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYxJKVTOuA$ 
https://urldefense.com/v3/__https://www.youtube.com/watch?v=5ciDNfmvMdU__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYzcy6BrhQ$ 
https://urldefense.com/v3/__https://www.youtube.com/watch?v=9pDddxB7LbE&t=3022s__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYzc81qwFQ$ 

[3] Altenkirch, Thorsten ; Kaposi, Ambrus ; Shulman, Michael ;
Üsküplü, Elif Internal relational parametricity, without an interval
In: Bahr, Patrick; Møgelberg, Rasmus Ejlers (szerk.) 30th
International Conference on Types for Proofs and Programs : TYPES 2024
– Abstracts (2024) pp. 56-58. , 3
p. https://urldefense.com/v3/__https://types2024.itu.dk/abstracts.pdf*page=66__;Iw!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYyPBrrdwA$ 

[4] Michael Shulman et al. Narya: a proof assistant for
higher-dimensional type theory. Code available on GitHub:
https://urldefense.com/v3/__https://github.com/mikeshulman/narya__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYzxIitYNw$ 

[5] Budapest type theory
group. https://urldefense.com/v3/__https://bitbucket.org/akaposi/tipuselmelet__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYy28c9a6g$ 

[6] Faculty of Informatics, Eötvös Loránd
University. https://urldefense.com/v3/__https://www.inf.elte.hu/en__;!!IBzWLUs!WZqIna451o_Y6678ooKuKnddewav7OPubVFGf-NQtWxn14WNyx9tg0CuApuVaLqQu2qm1IhFkWB9Oy3pqJ6nymHvf8PjfYy9-VnQmw$