Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Ambrus Kaposi <kaposi.ambrus AT gmail.com>
  • To: types-announce AT lists.seas.upenn.edu, Homotopy Type Theory <homotopytypetheory AT googlegroups.com>, coq-club AT inria.fr, agda list <agda AT lists.chalmers.se>, eutypes AT cs.ru.nl, epn-all AT inria.fr
  • Subject: [Coq-Club] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary)
  • Date: Wed, 29 Jan 2025 11:00:09 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kaposi.ambrus AT gmail.com; spf=Pass smtp.mailfrom=kaposi.ambrus AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f48.google.com
  • Ironport-data: A9a23:22CIo60mcPaGcFaLlfbD5Zd6kn2cJEfYwER7XKvMYLTBsI5bp2YDx 2IbWmjSbKrfNmrzLo0jboS18ENS6JDQzt9qHVdp3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn8gFaYDkpOs/je8Eo17ayr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW2vjntdpLWI9B90Bq8xnWTh15 P4lLhlYO3hvh8ruqF66Yuxlh8BmM9OyeY1D6jdvyjbWCftgSpfGK0nIzYUAjXFg24YUR6+YO 5pxhTlHNHwsZzVMM08QE5N4leKinGTkWzJdoVOR46Ew5gA/ySQriOWwbIOOIYLiqcN9t2akv EmbuEbDO0smbtyzxBGJ23yUv7qa9c/8cNlPTeXnp6ACbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xYA/7EruR935dwappWaN+B8aQdtZVeMggDxh0YLR6gedQ3ceF3tPNIxgu8gxSjgnk FSOmrsFGACDrpWFRi+/8Za3pgniIHk/PTdbXj4GcA0stoyLTJ4IsjrDSdNqEaiQh9LzGC3tz z3ikMTYr+VD5SLs//XrlW0rkw6RSo71ohnZDzg7s0qg5wJ9IZG/PsmmtQid4vFHI4KUCFKGu RDoevRyDshfVvlhdwTUH43h+Y1FAd7balUwZnYxRvEcG8yFoSLLQGypyGgWyL1VGsgFYyT1R 0TYpBlc4pReVFPzMvQnO9LgU5V7kPSxfTgAahwyRoofCnSWXF/XlByCmWbKhwgBbWB1wfFha MjFKa5A815HUPk2lVJauNvxIZdwm3lmmjKNLXwK5xug1rWaaTaUT7xDWGZinchohJ5oVD79q o4FX+PTk0s3eLSnPkH/r9RPRXhUdiNTLc6t9KRqmhureFsO9JcJUKeJmetJlk0Mt/g9q9okC VnnCxEAmQSl3SSdQehIA1g6AI7SsV9EhSpTFUQR0ZyAgSNLjV+Htf9EK8kEbvM8+fZ9zPV5a fAAdo/SSr5MUznLsXBVJ5X0sIUoJlzhiBOsLhiVRmE1X6dhYAjVpf7iXA/krxcVAgSN6MARn ryH1yHge6QleThMNsjsVa+Q/wuDhkRFwONWdGnUE+ZXY3TpodRLKTSur/oZIPMsCBTkxxmc3 Tm4GR0z+OvH+dc01PLrhqm0iZijPMUjP0hdHkjdta2XMwuD9EWd4IZwasS6VhGDa3HVoYKJe vdw48znFsE+jHJmktZZAql666AT/P7trOJq9RtlF3D1cFibMLNsDX2Y181ptKcW5LtmlSape 0CI6P9IEK6oPZ77LVsvOwYVVOSP+vUKkD307/5uAkHb5jdyzYWXQ3dpIBiApyxMHoRbaLp/7 78ah/cXzAijhj4BENWM1HlU/lvRCE0wafwss5VCDbL7jgYu9Ep5XqXdLS3L+7CKVcRHNxg7A z2ThZeavY9m+Gj5TyMRG0TOjM1nvrZfnDBRzVQHGUaFpcqduN8zwy9q0GoWSiZ780x59txda 0lRGW97H6GsxwtTpdNiWjmsEj5RBRfC9U3WzUAIpVLjTEKpdzLsKWEhCNmJ52Qc1XxWRRlA3 bSi0G2+ey3bTMLw+SoTWEBetP3oS+JqxDDCgMyKG8ekHYEwRDjY3ouCQHUukAS+J+8cn2jFq vtO0McqTJbkJAgCp6EfIKuL54Q6ERyrCjRLfqB8wfkvA2rZRgCX5RGPDEKUIeZmOP3A9B6DO fxEf85geUy363eTk2o9G6UJHr5Tmcwp7vokfpfABzYPk5mbnwpTnKPgzArMr051fIw2iuc4E J3bSByaGG/JhXd0pX7EnPMZBkWGO+s7dC/O98Hr1t4WFqAzkvBmKmAz9bqWg0+7EiVa+zCsg QeSQJOOksJDz9x3kprOA5dzIVy+CenOWdSi9CGxtNVzbu3zD/reijNNqnfbElRXGZAzR+VIk a+8tY+r/UHd45czfWPru7iAMKhr+fSNWPFzAs7mCUIDmA2uV9LeuUodyTqoLbhMts1X3ei8Z g6CcMDrX8Uka9Rc43x0aiZlDBcWDZrsXJrgvS+Qq/etCAAX9B7udveLxCTMVn5KUBMIN7nVK B7Gi9z36v929I1zVQI5Xdd4CJpGEXrfcKoBdeypkwKHD2Ot02iwipG7mTUOsTj0W2S5SuDk6 pf4Rz/7RhS4mIfM6Pp764VSnBkmPExRsNkKXHA22oBJ0mihLWs8M+4iH40MCchUngzMxZjIX mzxQ1V4OxrtfwZvUEva28vibDe9F+ZVG9beJx4VxW22RRqyJru9BOpGyn89zVZwIzft9bTyY 5VWsHj9JQO4zZxVVP4erK7zy/tuwvTBgGkE4wbhmsj1GAwTGqgOyGcnJgdWSCjbCIvYoS0n/ 4TuqbxsGylXiHIdEPqMv1ZQERAd+Sz1lnAmMXfJz9HYtIGWiuZHzZUT/g01PqIrNKw3yHwmH BsbhFdhJ0iZ33USve0ivNdBbWpcF6eQBsbjREP8bVR6okxzg1jL++sNmCMOSIcp/ws3/5YxU NWzyyBWOXlp43y9FFFbJcvlNn6xvr8x4+n1sTPC
  • Ironport-hdrordr: A9a23:6Ohauqn/tKpPxJUXeKonjPjSOD3pDfL/3DAbv31ZSRFFG/Fw8P re5sjztCWE8wr5PUtLpTnuAtjnfZqxz+8R3WBzB8bbYOCFghrQEGgK1+KLqEyDJ8SXzJ8/6U 4KSdkYNDSfNykfse/KpCa/CMgp29SK/eSFgu3E325xQQwCUc1dxjY8JALePEMefmd77FkCe6 Z0JPArm9NtQxUqhw2AZkU4Yw==
  • Ironport-phdr: A9a23:imOK3Rd8m2wosssyK+okZnnllGM+U9bLVj580XLHo4xHfqnrxZn+J kuXvawr0ASTG92DoKga26KW6/mmBTdZp87Z8TgrS99laVwssYYso0QYGsmLCEn2frbBThcRO 4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+M Ai6oR/eu8QYn4duMLo9xgfGrndWeulbxn5jKVaPkxrh/Mu985Bu/zlKt/4968JMVLjxcrglQ 7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus8 6lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZ IYUEeEPIfhXoJX8p1sWrBuxGw+sBP/0yjRVgnP6xLA23/g9HQ3D2gErAtAAv2nOrNjtNKkcT /27wqfLwzrMc/xY1izw6JTRch07vf2AQa58fMjXxEIyFw3FlFKQqYn9Mj6J0+QCqHKb7/d7V emyjmAosRlxoj+0xsctl4LEgYEVxUrc9SV+24Y1JMe0R1R+YdG/CptQqjqaOpB5QsMnWW5ou SI6xqcatp68eSgH0ZIqzAPQZPKbaYaH+A7jVPqPLjdignJoYKyyigix/ES+1+DxVMa53EhKo CdBj9XCuG4B2RLS58SaRfVz8EWs1DaL2g3N7uxJP0M5mbbVJpI/3rI9kp4evEvFEyTrlkv2i 6qWeV8l+uiu8+nofLHmpoOCOINuigH+L7wildG4AeQ5KAQOWHKb+euk2L3450L5RqhFjvwon anWt5DWP9oUqbOkAwNN0ocj7Au/Dyu70NsDg3YLNk5KeBWCj4TxOlHOPO34Ae2ijFSviDtry PHGPqHhApXQNXfPiqvufbF460JE0wUzzMxf6IlJCr4dI/L8RFPxuMbfDh8jPAy5xfvsBtZl1 o4GR26DHquUPLnRvFKI/O4jPfeAaJIPtDvyKPUp/+PigH87lFMHYKWk3oYbZGqlEvh7PUmVe 3jhjssHHGwXoAc+SPHqiEaeUTFNfXa8QqM85zAlB4++EYvOQJ2mjqab0yehBJJWY3hLClCSH nfscIWJQ/IMZziTIs9lizAFW6KhR5I42RGguwL3yKBrLuXT+i0fupLj0MZ66/fPmhE18Dx4F 8Wd02eTQGFohm4EWSM60aRlrUF+ylqPy7Z0j+JFGdBJ6P5EUR82NZvGwOx7D9DyVBjBftCMS Fu+QdWpGykxTtUqw98PeUpyAdCigQvZ3yq3GL8YjLOLBJku/aLd23j9Pdpyy3HD1KU5iVkpW dNANXe6ia5n6wjTG4nJnl2Hm6qyb6QTwDbN9HufzWqJpExXTAlwUbzcUX8DYkvWsM/261jZT 76uDLQnKhFOxdSDKqtMcN3pjE9JSO3tONTEe26xgXu/BQ6UxrOQa4rnY3sS3D3bCEQdiQ8T+ XKGOBMlBiahpmLeFCZhGUjuY0Pq6+l+qWm0QlU6zwGQPAVd0O+p6wYYnrmVTfUUw7QPtQ8lq i5oBxCm0tvNTceYqgxnOqhQfJd1wFBC0n7erx01Ao24IuhehlMZaRU/60Pp0hJrDZ1Rjdkyo W8qwQ1oOIqX11ROcz6Xx5ftIqaRIW73qlTnYKnPn1razdy++6EV6f1+pU+n9AimGkNq93R8z 5EB2nSQ773ODREOStT6Uk8z8hVgvPfBb395r47JyWx0PLKcuSSEwc9vAu9hghu4eZJWNKesF QnoEsRcCdL9BvYtng2AaxgeIfsa16csONinP6+F0basJ+cmlTesl3lcyI9420OIsSF7T7ibj N4+3/iE017fBH/Hh1C7v5WywNgcDdlzNm+2yCy+QZVUerU3Z4EAT2GnP8ywwNx6wZ/rQX9Rs lC5VBsdwMH8Xx2UYhTm2BFIk1wNqCmkkDO/1D0ymjQjtLeE9CPLyuXmMhEAPz0DX3Fs2G/lO pP8lNUGRA6tZgktmgGi4BP5zrBcv6U5JmzZW1pTVyfzJmBmFKC3s+nKeNZBvbUvtygfS+Gge RaaR7r69gMdyD/mFnBCySoTcjirvtDmhUU/hj7Nanl0q3XddId7whK3CMX0Y/lX03JGQSB5j WOSHV2gJ5yz+t7SkZ7fs+e4XmbnV5tJcCCtw5nS/C28rXZnBxGyhZXR0pXuDBQ63Cnn1tJrS TSArRDyZZPu3ri7NuQvd1dhBVv14c53Uo9klY54iJYV0HkczpKbmBhP2WT6KdJA2OT3aXAXW CUjzNvc4Qyj00pmbzqIy4//SnSB0555fdDpBwFekik57s1MFOKV9OkexXoz8gf+91iIJ6Qtz VJ/gbM05XUXgv8Eol8oxySZWPUJGFVAeDbrnFKO5sy/q6NeYCCud6Kx3Qxwh4PEbvnKrwdCV XL+YppnEzV365A1M1vU12byrIjhcsPNdvocsxSVl1HLiO0fe/dT3rIawDFqP27wpyhvyOcji gdvm5i/tpKaME1i+au4BlhTMTi/NKZxsnn9yK1ZmMiRxYWmGJ5sTy4KUJXfRvWtCDsOtP7jO m5iCRUEo2yAUfraFA6bsgJ9qm7XVoqsPDeRLWUYytNrQF+cIlZeiUYaRmdykpk8HwGsjMvvF SUxrjMY/lnjq11Fz+hyKgLXXWLWpQPuYTAxAJSSNxtZ6Ahe6lyda5TPqLIuWXsCp9v9/ESEM SSDah5NDH0VV0DhZRirJbSo6dTasqCZCue4M/rScOCLoO1aWe2PwMHn2Y9n8jCQc8SXayM6X rtrhwwZByk/R5SK/ldHAzYanC/MccOB8RK1+ykt69u67OyuQgXko42GF7pVN9xrvRGwm6aKc eCK10MbYX5V0I0BwXjQxf0RxlkX3mttfiGqCrVGvCvHVr/LsqBSBh8fLSh0MYEbisB0lhkII sPdht7vg/R7h+YyEFYDXFnrgNyyTcMPKmC5cljAAQzYUdbObS2OyMbxb6SmTLRWh+gBrBy8t wGQFEr7NyiCnT3kBFi/dPtBhyaBMFlCqZmwJ1xzXHP7QousOXjZeJdnyCc7yrouijbWOH4AZ HJiJlhVoOTY7DsE0K4iXTUQtjw/cbbCw2HDs6HZMspE76ctWH8v0bsEuDJijOIEiUMMDP1tx HmM8Jg3+wvgyq/XjWA/GBtW9mQV2sTR4RQkaf2frt4aAT7F5E5fsj/WUkhM/oo/TIWo4vA1q JCHlbqvemgetYuOoI1EQZCTcZzPMWJ9Y0OxSHiNU1RDHXjzcjuGz01FzKPLqSbT98lm7MCqw N1XFNo5HBQ0Dq9IUBw0WoxfZs4tDnV81ufExM8QuSjk9UeXGZUc58GdEKrVWKSnKS7F3+MdO V1SmuK+dt5VbsqiiikAIhFslYDOUSI8RPhrpStsJk8xqURJqj1lS3ErnljiYUWr6WMSEvi9m lg3jBF/aKIj7mWk5VB/PVfMqCYq9St50dz4nTCcdiLwJ6asTMlXDSTzrU04LpL8RU58cwSzm UVuMDqMSahWivNscmViiQmUvpUqe7YUVapffBoZ3u2afd0t2FVY7zq9nApJubuDBpxlmw8nN 5WrqjMI2g5uasI0Ob2FJKdNyQs15OrGtSup2+YthQ4GchxVoSXCJWhS4hVOaul1QkjgtvZh4 gGDhTZZLW0FVv5w5+lv6lt4IeOLiSTpz79ELEm1ce2ZNaKQ/WbaxqvqChs90F0Fk05d8P14y 8AmJgCXXlgo17rXHhEDL9fZAQ5QZstWsnPUeGzd1IeFiYIwJIi7Gu3yGKWWs70Ih0u/AAszN 4EF78BEAYP1lU+EfYHoK7kKzRhr7wPubgbgbrwBaFeAlzEJpNu6xZl80NxGJz0TNm56ND2++ rfdogJCaBurWd43ZjIFRNJBOC5mHsK9nCFdsjJLCzzliorxLSCN6jb9omLbCzyuN7KLi9+bY BptDJe9/jBtqsCL
  • Ironport-sdr: 6799fc2c_Dw4RLD84rs/JEA8bxyHuGi9lqyMhRumAThgtcHjMlDZloEi DagwuNdsXv6LIhFqY1FrGWf3MmYq8EHD1kN06uw==

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


  • [Coq-Club] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary), Ambrus Kaposi, 01/29/2025

Archive powered by MHonArc 2.6.19+.

Top of Page