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

[Ambrus Kaposi <kaposi.ambrus@gmail.com>]

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@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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/HomotopyTypeTheory/875xlylz2u.fsf%40neumann.mail-host-address-is-not-set.