From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE,URIBL_SBL_A autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-ej1-x637.google.com (mail-ej1-x637.google.com [IPv6:2a00:1450:4864:20::637]) by inbox.vuxu.org (Postfix) with ESMTP id E2D58212AC for ; Wed, 29 Jan 2025 11:00:20 +0100 (CET) Received: by mail-ej1-x637.google.com with SMTP id a640c23a62f3a-aa67f03ca86sf548614466b.2 for ; Wed, 29 Jan 2025 02:00:20 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1738144820; cv=pass; d=google.com; s=arc-20240605; b=COJLdYzjuSD/vt4+2PyAeQ2aXmX5D8TYgkuAbsLH/0WCPvO3zbCJqliSRM9NqH9HX8 3hOIkVFLXL8MNn2HumIY4uoWqvQIltAGM6syRozlNE1Hkt9nKjS0v38aANGhVS9HkFWY ulrfdoqltclKTWRhXMgFvZV0MIseyBZjQX3pVSIhhygCZN4h9OXvaul5rkYAJqyog5EI m7l5MzFfeInDae2RFLKIw6fOkDRG2LSuwGFHAPQ6+5Onhyi43JxWanHo3gqPzV3zWDWR mNDhctJh4ygt7NbA4N9lRl/Y3ZhFLiHg1wo480wBP3o4n3rDxXZduOgSufRTgeU2S0fB 5jxw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-transfer-encoding :mime-version:message-id:date:subject:to:from:sender:dkim-signature :dkim-signature; bh=Q4jPDSmkQiKPfncNcwjy0RrdrG033Xuu0Hl6pUTVnuw=; fh=TKjbBMI1Uu1ImyRQgmXOZ1UPUi70613rKoRxp7FsF5Q=; b=YUg14Z5TRRPuHmT8gEXW0xENFPjYirhEwAhZT+DAyIQOiTXVLgPvH9OF4QHjcCI+Jm mKyOOMQ6UlLkbkDWqGyccfJn13VG9pjzhJxtyObfG6Gjl7kR0rCm69P8BCA3DV3TJp5j 8PUD32lNdzme///LKtGabL46AivSAbpL+AVLzvymCoyJ98CEkmzOxMXF/UMp8YtGRIWN kUtUQ8PFrE+dQ8yVmsZRxW0+JWTRQHbpxbwqNk5IEJGG/bcmg+bSOndzghL2XakPvkhY eBYDnqUwRr7Ht5T6KtqppaRIcPPRcHP20i22UYFXMQar+FWiH5n8RyrsY1U+OHO4akJy /fBg==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=eMaOx7US; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::42b as permitted sender) smtp.mailfrom=kaposi.ambrus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1738144820; x=1738749620; darn=inbox.vuxu.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:mime-version:message-id :date:subject:to:from:sender:from:to:cc:subject:date:message-id :reply-to; bh=Q4jPDSmkQiKPfncNcwjy0RrdrG033Xuu0Hl6pUTVnuw=; b=nP9f0kr4ZVHiAgrsGnqOXjYQ14PFTOB9LmDz7i72Nik9vZbD0bO5/dPJZ7/suGmWS6 tRvVLG3Nc8Lrtqh4Y3BFyl5t0Zm4JyY3xWlV0HKUo2//baj6/L1wBWwp63yjTwFgIN1g RkF2XYNue7M3wTnjSyqK1MDRrY1rY7+FyVTzLhpRYfiDGVk1ueiu/U8lZfimXkMwIHM9 G1MOlWrEhLhzVgyCw6MTre0PHZFRTOxbCDSdJVuf1ybKBBPf+9bmn4C6ORNrLeOOCpnQ gjQcf05cZ9PNgknrEj9lG2BeLHhcskDYwf+s4i2E933A/T1QJhL04QqxhriQG4++CLY6 ejiQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1738144820; x=1738749620; darn=inbox.vuxu.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:mime-version:message-id :date:subject:to:from:from:to:cc:subject:date:message-id:reply-to; bh=Q4jPDSmkQiKPfncNcwjy0RrdrG033Xuu0Hl6pUTVnuw=; b=iwNJFAv9oBwAFgV4tkkSyMXtCkPopJJGBQelwpJSLcjSjJhCYR5QzNi9JTsJ5UsEcA dPPBnl3IJQUE0N21ymjiPoezQSk9Uw1OZ/x3nsHyzvlfETpACux2gfnxwEN82Np/jXtt 1S6r7NUUjwteKdNDyAkuCKCJbW7pmaTPvqXisca7CZTeljYs2mIV4ELaB/uVWJZ8Ghce 2G5csQUGVSRCPPTmIRVi2J6r+d7BaXAWYeIm+Q8q8LxJat6baBqHb8xAAYBFZ6IVilD2 bmP/jatXAm6f6fHlCQyqby042aBhTnpClTYW3rTpUNbxuhSke24VCGJZ/NsHRTbElALl 4+8w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1738144820; x=1738749620; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender :content-transfer-encoding:mime-version:message-id:date:subject:to :from:x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=Q4jPDSmkQiKPfncNcwjy0RrdrG033Xuu0Hl6pUTVnuw=; b=Yr7oQnpTdXoWSHpKyydZ45rGATBGMiDMBRmvsPpGTIijKzJCDk6WXMaJibsuWJ63oX t/qTTDTgmoJzApe7NFokkGNn5qoyPtD40IqXZdjYz/GtEsJIbLEUTcvszoqCyZH5G8a0 AH29TMAXPPMob4cW0msTil5J9E+fyzPLYlbUP9uabFaIBo9EQDJsZkes+/uwxY54jIp+ GwUQYLRxrwaE2iPodVV2eItA2xrjhxXeQv22skGZ+EvaqkiruKzFxkmRpPP/nA6lRUS4 qwlZA85yEz0w0cwWXwSMCHJNxIQck6pPFvERz6YGoQ4ArfeWHTwIFVX28Db8UsDVCjOM gCUw== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCXbr+F/vqbwaslQoVAP2xfClg+1zdem9KIN5ZY5banGWYtbDsqpDv2Ez0ulxVr+IQ7gBA==@inbox.vuxu.org X-Gm-Message-State: AOJu0Yx79eRcQizf42SisX35DVKzv+D5np6zZZ3jWRvK7pPsd6mqu6kM qvejQ1Oihg5YcPy9d0K/EoaPKo7fUfdnOEN9PTDtCdfAXTfSUZN2 X-Google-Smtp-Source: AGHT+IHPqDnkBqKSH/NQitDYT80XdHiQ4GVF2DkRZZfMkbqsLohG/KTadkRts7wN7bbjuMPhLLvv7g== X-Received: by 2002:a05:6402:5205:b0:5d9:ae5:8318 with SMTP id 4fb4d7f45d1cf-5dc5efec050mr5147370a12.20.1738144819268; Wed, 29 Jan 2025 02:00:19 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:9f6e:0:b0:5d0:e7a4:9762 with SMTP id 4fb4d7f45d1cf-5dc5b135f58ls107789a12.2.-pod-prod-05-eu; Wed, 29 Jan 2025 02:00:12 -0800 (PST) X-Forwarded-Encrypted: i=2; AJvYcCVGcrWNbNRiu0ywZMQbmNvWIDjBGDecNJ8WEW1pl2QEG5Fw7Qk9Hf32sW6Ylk06UEkkgV2xvXdYVr0umV3Cqrph65E=@googlegroups.com X-Received: by 2002:a05:6402:3584:b0:5d0:ced8:d22d with SMTP id 4fb4d7f45d1cf-5dc5efec0d2mr4808167a12.22.1738144812029; Wed, 29 Jan 2025 02:00:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1738144812; cv=none; d=google.com; s=arc-20240605; b=aM7J1a78EsBkxCHipXBxDMhc2vnSwyQ1GudLWXmxyQXf46TZvd/bU3cX7XuXSk+MRg ZWQAHofm+DQvgbwvz3tefJYr68Sj60UazlXZhm4L/lX5/ggmK107LzUrFlVouAZZkzMC ZMlAxaL8FcrOGc12Vg2TasnLTQSAiCTE2/hiw4UYViWYZgKVaU4SOIyDr2gIO8u45tHl 5qMc4n/izJrfJ2BUPXsb/qN+9esD+tsKxNt6gX1reSWLpAbrXYije/c4pby7BAHCkvkM FIXVDnMgwO62KQj0x2SUuJpuyfNucCpCqp6XS625qYR1AaMMrLhPYoPlqrjfyz61YUiu Mwqg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=content-transfer-encoding:mime-version:message-id:date:subject:to :from:dkim-signature; bh=uSNHRIeAhgqNSz9Ocb0y7+tYk165Qysw7OY7gYi1d4E=; fh=pHVTcu+0A6m/Nef5HyoY/JQ4gEQb0EXJCaNvJOtARj0=; b=BcYmRv1AkZN+ZuyIUPfIkZmLiwJWSOti6rgyBQi3i0aEcKkcNIkVpk7Xu3bNXdAMNI apSEcJDok6fNZpCunV/tUbEk5Fjp+BFsl3MIQ50+Ih47uLKlQ3YFM/tH9H0I5UOQ5Mbj IW2tiJ9Ix4X5M9QEUw6xwSxnUM12mECTGL48vJz4xjza6auC87WKwZs4bX/urXLQ64w5 78DJGD5h/No8LvvgmPaQCBQMlY5igdKUNtjwWW2mExTRSPEhxQJrR6ZMf02jzxWMYkOG V/jxYoEb8ugDgQrNSdIgnQFe6ddkdYWynFGSv8g8wPkKo/Ly92apUGYS3BvccWFGvMny 6bVA==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=eMaOx7US; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::42b as permitted sender) smtp.mailfrom=kaposi.ambrus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Received: from mail-wr1-x42b.google.com (mail-wr1-x42b.google.com. [2a00:1450:4864:20::42b]) by gmr-mx.google.com with ESMTPS id 4fb4d7f45d1cf-5dc186283ffsi273917a12.2.2025.01.29.02.00.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 29 Jan 2025 02:00:12 -0800 (PST) Received-SPF: pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::42b as permitted sender) client-ip=2a00:1450:4864:20::42b; Received: by mail-wr1-x42b.google.com with SMTP id ffacd0b85a97d-38a88ba968aso6477450f8f.3 for ; Wed, 29 Jan 2025 02:00:12 -0800 (PST) X-Forwarded-Encrypted: i=1; AJvYcCUcFomQXEbcsZFmzIBo+mu8zZ9TJqYymLS/OeTVhue4OP5thXX5OSMY4/NX+y1WvRYsePbkYedizt9CljXX5S6mNQw=@googlegroups.com X-Gm-Gg: ASbGnctlYz8i7GRuD2APK0pMxFyKiLeHOCFo66zU4ghgKEvZwOMCfuaLYy6d7a99lBN iyBsO/BB4cSVW1rvYBlMqDVpLaC6CzGXmAPS/zDuGdtna+HiYkk+y1Io+OnZBZMMTeGgbK57dYT dqAIawOms7YJoN0zb2fcbRliGQ34Q+eaHfhtI9kXPFLphh1ib1CPkTdOXNfvtD257++2qNccG6K oPme/fL5224OkM8Mj4KH4PK8Km3sqXnaADNzq9TT4xsphNO5RFBiqpuHJCLn50LY1C08MNctiJw FFLxDApe9Hw7QdbT2PEu7bgERgfA6kP/1i76Ol3qQ47weIFb X-Received: by 2002:a5d:598c:0:b0:38a:50f7:24fa with SMTP id ffacd0b85a97d-38c520a682bmr1962282f8f.54.1738144811126; Wed, 29 Jan 2025 02:00:11 -0800 (PST) Received: from localhost (client-112-70.eduroam.elte.hu. [157.181.112.70]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-38c2a176449sm16721059f8f.11.2025.01.29.02.00.10 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 29 Jan 2025 02:00:10 -0800 (PST) From: Ambrus Kaposi To: types-announce@lists.seas.upenn.edu, Homotopy Type Theory , coq-club@inria.fr, agda list , eutypes@cs.ru.nl, epn-all@inria.fr Subject: [HoTT] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary) Date: Wed, 29 Jan 2025 11:00:09 +0100 Message-ID: <875xlylz2u.fsf@neumann.mail-host-address-is-not-set> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: kaposi.ambrus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=eMaOx7US; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::42b as permitted sender) smtp.mailfrom=kaposi.ambrus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , 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=C3=B6tv=C3=B6s Lor=C3=A1nd 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=3DFrxkVzItMzA https://www.youtube.com/watch?v=3D5ciDNfmvMdU https://www.youtube.com/watch?v=3D9pDddxB7LbE&t=3D3022s [3] Altenkirch, Thorsten ; Kaposi, Ambrus ; Shulman, Michael ; =C3=9Csk=C3=BCpl=C3=BC, Elif Internal relational parametricity, without an = interval In: Bahr, Patrick; M=C3=B8gelberg, Rasmus Ejlers (szerk.) 30th International Conference on Types for Proofs and Programs : TYPES 2024 =E2=80=93 Abstracts (2024) pp. 56-58. , 3 p. https://types2024.itu.dk/abstracts.pdf#page=3D66 [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=C3=B6tv=C3=B6s Lor=C3=A1nd University. https://www.inf.elte.hu/en --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/HomotopyTyp= eTheory/875xlylz2u.fsf%40neumann.mail-host-address-is-not-set.