From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 31732 invoked from network); 4 Mar 2023 10:16:33 -0000 Received: from mail-wm1-x33a.google.com (2a00:1450:4864:20::33a) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2023 10:16:33 -0000 Received: by mail-wm1-x33a.google.com with SMTP id az39-20020a05600c602700b003e97eb80524sf4046826wmb.4 for ; Sat, 04 Mar 2023 02:16:33 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1677924992; cv=pass; d=google.com; s=arc-20160816; b=lK4Rf+Eg/tn1RVe7Ez/Ul/0JpqRqGaANgXvasNfFX4hfDw6ouvmROnMkREATr1f1BC YsdjvkR7FD0hjkzVT9aFMlxFDc8UMtwVRA8P7KsRSGj28/VvfNmr4ClxVchlVOeGubEQ /oZdEAacNtfq1C2j5iBf6l11pQEfZR0C2T7VHNgmnIohzdVH45NMoGnC72RJUtXoHxyh o+MfnuxfmavttlYP4JFqJnD55XfU7R8JSbVqWugK4MqtYEJMCU+bJOe6J+ciIysUtSD/ 0cLGaOiHi992FLWIdc7fHjVPEdgNzFx9WK81bbgd3rhRHxzkVGRQKpCm3fM1UAnhpP85 eYmA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-transfer-encoding:subject :from:to:content-language:user-agent:mime-version:date:message-id :sender:dkim-signature; bh=eqxfHZgdyKfSqOm1/yGAheMK6C6R3buSIBlI1PPtpGs=; b=MA7FGkgeJFyt8QF6934KirCo08X4Pfq7zJgShJ7x1TsCW3yZHgBQYmBFG0RoQ2ULqX 5kGFWEhVP/fiFgRD2Ez4bRtnz4C+JJNvRP2tGNhMMQ/arvyaxCAWo1BtUdhEyBdr3hVf GDifE5OhM/DCcmkNamnd868Y9VJYVA8w+QpGw+BhCrfq259f1MHIV7e7xPTshA8i51vp JfxlyYfiL3edSoxw/a7q1GaR1xIkdNF5rrW8ImmE3ybMop1AfH/dbjOLLrq6GLTiH0FI 31pmnVGxWPkDpk6yx1qdkSRquHp/Kam/u0dy6BRirk+W/QX5wXO3PrlmqiSrye7JDlgw 3uyA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=B0QKjFPY; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=inria.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; 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:subject:from:to :content-language:user-agent:mime-version:date:message-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=eqxfHZgdyKfSqOm1/yGAheMK6C6R3buSIBlI1PPtpGs=; b=dFyGfY7PhIObTah0Fb2nXiTB3VaeJ/jC3bDmrcqNrvgJnX6kHFhv4+7pHmq6s3kHLy Uoui54p4T0kmvyFQZd6WDIVbIxIEvg/1T2xaZJm/OgNB6jCqLS1Ol+Sogw7wURXiuuR/ XQ9/Jfcsoa+eXVm8hySaQzTxMJMamIs8S/EsqrNARYIpDT+OPh9roWHak2G1HYIvrJlk 9bEBYZ3KV7dOtJ/ku40GV2j3mmMbpoO8yZ9yiszYQV6y+37jglNpLIkz4stL7FHnqG3R /ROR8TRVoZgi68O/PxaFMG18yh32DgSfZ8WtUPTpuQDQpKDMvL87v/kmg6Ml9v/6Om7T yveQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; 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:subject:from:to:content-language :user-agent:mime-version:date:message-id:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=eqxfHZgdyKfSqOm1/yGAheMK6C6R3buSIBlI1PPtpGs=; b=RBVxYF01l/ozMpUFdbTqmxo8IjQO+X5bZFpQkndKpkbH8dQA/wPAUS8K+XuBS1ffUp ixf2qaPENJ7i0UpFsuPQs+qc8GvEb5rs2Rp4x9VeTftYUetJ4ca3iPcKnKUyfERR0QiQ AXEqJwmOEJGAl4Yf/glxq6gorE9tYSWZvlsrE8zwZlVbtni4GHTyVJpoCJtO7oxyxfgK FQ460RHFrsKlbRFPJCVzzDIKw4kNRUTof7OdhJG3qWEFu7Zm6j1Zdjxnjnk6fLLeQen5 +UTy27YKSqg0H9AT6Me8tOz30pckfloATg1OmengtLh5xkC+oo5X5gGRKILmqpFDgTyH 9iaw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKXSm/DpXyFS39U46VjuREU6NO7qIoygq1a+nNru45I67cLAki3u kNxWJo5vGYmmRF7+N6LAUBs= X-Google-Smtp-Source: AK7set8vZq9diaNBM1g/GdRqe56Yr4Z8OzaPYeAySr95ATzb5w996t/KiSCdoXPuaknK0P5Sj4snoQ== X-Received: by 2002:a5d:4292:0:b0:2c7:1c37:22f with SMTP id k18-20020a5d4292000000b002c71c37022fmr1064398wrq.12.1677924992083; Sat, 04 Mar 2023 02:16:32 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3b9a:b0:3cf:9be3:73dd with SMTP id n26-20020a05600c3b9a00b003cf9be373ddls4376680wms.3.-pod-canary-gmail; Sat, 04 Mar 2023 02:16:29 -0800 (PST) X-Received: by 2002:a05:600c:524a:b0:3eb:3998:36f7 with SMTP id fc10-20020a05600c524a00b003eb399836f7mr4162912wmb.8.1677924989846; Sat, 04 Mar 2023 02:16:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1677924989; cv=none; d=google.com; s=arc-20160816; b=Y1ICdvhzw7TrYYxDSPS0ou8gUAZDBDwUX/l4vcRijFYnHzaF0pOltjUEzRuJks6JWT zNHi5OjnaS+w0vYHh6AZaOMr13YAfGvs6eEGd9/tX49pYx970vclwq+KBa0U7N2j/ZYd AtkZvoEI2BgRZ3lpT5kDrlnnt5sw9TeoN4smGHdBrfap9bOIiHc3FOVvpH/naTx0jRbo 85l+5MVDSKNgYMj6V0ZvDMliMa4KWz4mM57J6Zo4pjVIsf8E9uXH60lyRBN49gEnE97k GfhaaiKodU0E4Ma9NxLOqBBwfrWQ9KJKkW0GSq484SsaMaMh2D2J+jfNaCjasasENZ2F bT1g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:from:to:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=axz/Z15CNHu3k34C23kTczomoyUOQ+WcBRxW7Rvh9Uk=; b=cVeVxUp42qNB6ejRvH78GGBmhu7qpV4iNMDRzl/nKC+6gdqXsi0mb2Sfi+YYxUjweU gwypmR3cGTK3Nh1vF2qrexVw4ERpyf27FkkSEtfMrU1XAhtDb1vNbNht+pi003W7sM26 lAaoyKfruRzc+y0FAB8TVWfoOn18IeaS4wVbr7BW/8/Q6mMHu+VlUNZuICYUL7IWjrxy ZZE+dFKfAAQ3+7p5YrNYM0gcjjAj/EI5KtyU1xUbtkLmaMat/OdTULlszF3IsnxqHal0 jPOzS0+9yxAUY7iztvnvB+qOcdiwKdkGmS1caSQBfbB12FizAjF7yrX7mPseBbYhbmaj otcw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=B0QKjFPY; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr. [192.134.164.83]) by gmr-mx.google.com with ESMTPS id ba19-20020a0560001c1300b002c6eaaaac82si189196wrb.7.2023.03.04.02.16.29 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 04 Mar 2023 02:16:29 -0800 (PST) Received-SPF: pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) client-ip=192.134.164.83; X-IronPort-AV: E=Sophos;i="5.98,233,1673910000"; d="scan'208";a="95409397" Received: from 176-137-227-239.abo.bbox.fr (HELO [192.168.1.83]) ([176.137.227.239]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 04 Mar 2023 11:16:29 +0100 Message-ID: Date: Sat, 4 Mar 2023 11:16:13 +0100 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.7.1 Content-Language: en-US To: coq-club@inria.fr, gdr-im@gdr-im.fr, types-announce@lists.seas.upenn.edu, homotopytypetheory@googlegroups.com From: Assia Mahboubi Subject: =?UTF-8?Q?=5BHoTT=5D_PhD_position_at_Inria_=2F_Nantes_Universit=C3=A9_=28F?= =?UTF-8?Q?rance=29?= Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable X-Original-Sender: assia.mahboubi@inria.fr X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=B0QKjFPY; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=inria.fr 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: , We would like to invite applications for a 3 years fully-funded PhD position within the Gallinette=20 (https://gallinette.gitlabpages.inria.fr/website/members.html) Inria=20 research group at Nantes Universit=C3=A9 (France). The successful candidate will contribute to the Fresco=20 (https://fresco.gitlabpages.inria.fr/) ERC project, aiming at designing fast and reliable symbolic computations. This project involves topics in program verification as well as in formalized mathematics. The start date is ideally in autumn 2023, but later dates can be negotiated. The candidate is expected to hold a master level degree in Mathematics or Computer Science before starting the enrollment procedure. Relevant keywords: dependent type theory, homotopy type theory, parametricity, type classes, hierarchies of mathematical structures universal algebra. Supervision: Assia Mahboubi=20 (http://people.rennes.inria.fr/Assia.Mahboubi/), in collaboration with=20 Cyril Cohen(https://perso.crans.org/cohen/) (Inria) ## Contact Assia.Mahboubi@inria.fr ## Local scientific environment Gallinette=20 (https://gallinette.gitlabpages.inria.fr/website/members.html) is a=20 large joint research group of Inria and of the Laboratory of Digital=20 Science of Nantes (LS2N). Research interests of the team include theoretical and implementation aspects of dependent type theory, extensions of the Curry-Howard correspondence, formalized mathematics, etc. ##Salary About 2000 euros monthly gross salary, including health insurance and partial covering of transportation costs. ## Location Downtown science campus of Nantes Universit=C3=A9. ## Environment Nantes is a vibrant city rich in history and culture, located on the estuary of the Loire, less than 60km away from gorgeous shores of the Atlantic cost and 2h away from the center of Paris by fast train. ## How to apply Contact Assia.Mahboubi@inria.fr before **March 31 2023** and attach: - a covering letter - a recent curriculum vitae - available transcripts (Bachelor and Master if applicable) - the contact information of two references --=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 on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/da449cf6-03b7-aa84-7037-894c7ffcd02e%40inria.fr.