Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary)
@ 2025-01-29 10:00 Ambrus Kaposi
  0 siblings, 0 replies; only message in thread
From: Ambrus Kaposi @ 2025-01-29 10:00 UTC (permalink / raw)
  To: types-announce, Homotopy Type Theory, coq-club, agda list,
	eutypes, epn-all

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.

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2025-01-29 10:00 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2025-01-29 10:00 [HoTT] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary) Ambrus Kaposi

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).