[Agda] 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://akaposi.web.elte.hu




[1] Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael
Shulman: Internal Parametricity, without an Interval. Proc. ACM
Program. Lang. 8(POPL): 2340-2369
(2024). https://doi.org/10.1145/3632920

[2] Michael Shulman. Towards a Third-Generation HOTT (Parts
1--3). Homotopy Type Theory Seminar at Carnegie Melon
University. Spring 2022. Slides:
https://home.sandiego.edu/~shulman/papers/hott-cmu-day1.pdf
https://home.sandiego.edu/~shulman/papers/hott-cmu-day2.pdf
https://home.sandiego.edu/~shulman/papers/hott-cmu-day3.pdf
Videos:
https://www.youtube.com/watch?v=FrxkVzItMzA
https://www.youtube.com/watch?v=5ciDNfmvMdU
https://www.youtube.com/watch?v=9pDddxB7LbE&t=3022s

[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://types2024.itu.dk/abstracts.pdf#page=66

[4] Michael Shulman et al. Narya: a proof assistant for
higher-dimensional type theory. Code available on GitHub:
https://github.com/mikeshulman/narya

[5] Budapest type theory
group. https://bitbucket.org/akaposi/tipuselmelet

[6] Faculty of Informatics, Eötvös Loránd
University. https://www.inf.elte.hu/en