From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 820E35D5 for ; Thu, 3 Mar 2022 19:06:07 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.90,151,1643670000"; d="scan'208";a="24293143" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 03 Mar 2022 20:06:04 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 31E6CE0B75; Thu, 3 Mar 2022 20:06:04 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 04DC9E00BA for ; Thu, 3 Mar 2022 20:05:58 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andrei.h.popescu@gmail.com; spf=Pass smtp.mailfrom=andrei.h.popescu@gmail.com; spf=None smtp.helo=postmaster@mail-qv1-f49.google.com IronPort-SDR: ZGN3C+RYHr7hNM9LoQn1ACW2oK9c75XBs+F9jyXCof5VWURrTRHJzSEd5GwTeL8ALeTgtwzIB5 8XtUmQ3AfzLLSME4D9w2t1d8Kjc51wvQqpqi0kORfcC38IONfXDmXfrqxPpV1c1yq0RDvx7RiU YjwW9sNUnkO1k1JqErMVdLRpDh3IqcEq6WaHVqPRo5+eFazw+HtYwF6tZ5XGrREEZJvp5f7nLF Cgfw70r1l+3DDKpN+REVs+X/1l0FBHBSfwg1RHYQUxl+8hMK1W8GUzP3lM17U8cLkzPllzyZpb HHgWCCa3N1XKWsZL1ElSVhtJ X-IPAS-Result: =?us-ascii?q?A0DUAwBwECFihjHbVdFaDnuBWoF6LjMBSlYsBAtEhFSPJ?= =?us-ascii?q?oFyjCqQN4F8CwEDAQ03CgQBAYkjAh0HAQQwCQ4BAgQBAQEBAwIDAQEBAQEBA?= =?us-ascii?q?wEBBQEBAQIBAQIDBAETAQEBDAsJBwgKAgUOAg4DYAFhAwFEgU+BTyULAzENg?= =?us-ascii?q?jUMGoN8BBEdARsJFQMSEA8CJgIkAREBBQEjNIJiAYJkAQMuD6BagQQ9izKBF?= =?us-ascii?q?QUXgQGCCQaBQAGDCAoZKA1nA4FYAgEGEn4shhGBI4MBhDiBBIElgUuCRIIwh?= =?us-ascii?q?h2CZQSVR4ECHVCBBQyBZpF0rioHg0uBQIlKlGEzqCeWVSCMc5QuAoUkECMSg?= =?us-ascii?q?SyCAgwHMxojgQGCOE4BAgEBAQ0BAgEBAwECAQIJAQECjicPg1mEcIUpRUQxO?= =?us-ascii?q?AIGCwEBAwmSawEB?= IronPort-PHdr: A9a23:1EsmNxQnucdMGdT00LGIxwjCUtpsouKWAWYlg6HPa5pwe6iut67vI FbYra00ygOTB8OCs6wP0rOJ+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtWiDanfL9+M BS7oQrMusULg4ZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQ bNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu8 6FmQwLvhykaMD456n3XhdJtg6xHvh2uux1/w5bKbIqIMPZzcb/RcdYcSGFcXMheSjZBD5uzY IUPAeQPPvtWoZfhqFYVsRuyGROhCP/zxjNUhHL727Ax3eQ7EQHB2QwtB84DsHLJo9XvKqgSU P2+wrPPzTXbcfxWwivy6JXVeR0mu/6MW69/cdDPxkkuDQ/Fjk+cqZTiPzONyOsNqHSU7/d7W OKgjm4osQBxojy1ysgwjYnJg5sYx1bZ/ip23Ig7P8e3SFJnYdG6CptQsTmXOpVrT848TWxlu CI3xLMIt5OnYCQH1okqyR7RZvGGboSF/x3tWeeMLTpmhX9pZrGyigi2/EWvxOPxVsm63VRIo ydDj9LCuHcN1xnJ5ciGTPtw5lmh2SuV2wDV7uFJJ10/m6nDK5M53LI8ip4evV7AEyL2gkn6k rKae0E+9uWn7+nqZKjtqIWGOI9ukA7+N7wjmsyhDuQ8NQgDR22b9v691L3n5EH5WatKguAvn qnXv53XId4XpqG+Aw9S3YYj7wiwAy2639QfmHkLNFNFeBSZgIj1I1zCPuz0APOlj1mvkDpn3 e7KMqDlD5nXIXXOlK/tfbNn5E5dzAozw8pf55VRCrwZOv3zXFL+tMbGAR84KQC0w/zrCM161 oMGR22PGbOWML7JvF+H4+IgOeiMZIsPtDnhLPgl4ubijXkillAFZ6mmwYMXaGykHvRhO0iVf GLggs0dHmcSogo+UOvqhUWeXjFJYnayW7sw5jU6CIK9EYfOXZutgbyE3CejBJJafGFGClaWE XfpbYqIQfkMaDjBavNmxzUPUeKJVpMl1Aqyr0nn17d3J/GS9yEF8drq29R8z+nSjg0pszd0B sCY3nuWCXp52isBXyct0aVXpU1m1kzFzaNjxf1WFJpX4u4PXgp+fZfA1Kl+Atb9Hx/ac82SY FmhRdqiDD4rSc8p2JkFZEM5U96rixSG2yuxH5cUkaaKDdo66PHyxX/0cu97x2zL1eEZiEErW cBSfTmvgKJl+gmVB8jRlF2UjK23XasZ1S/JsmyEyDzd7wljTAdsXPCdDjgkbUzMoIGlvisqL perALUjaU5azNKab7BNcpvvhElHQ/HqPJLfZXiwkiG+H0XA3auCOaztfWhVxyDBEA4ciQlG9 HCKLwU/QCfnu2XGASdlCHrgZkrt9a91r3boBlQswVSyZlZ6n6Gw5gZTgPWdT/0J2bdRsSEts Th1Wlb7x9XOBsGLuiJueaxdZZU251IUnXnBuVlbOZqtZ7tnmkZYcwlzuBb20A5rD4xbjcUwh HYjzQ43MLzBlV0dJnWX2pf/PrCRIW73lPy2Q4jR3FyWkNOf+6NUre89t02mpwaxUEwr73Rg1 dBRlXqa/JTDSgQIA9r3VQ4s+h52qqu/AGF17p7I1XBqLai/syPTk9MvCuw/zx+8ftBZeKqaH Q72GsceCoCgMusv01SuaxsFOqhV+stWd4uvcfec1a/tPKB4myqrlm9ayI9420OIsSF7T6+A3 poIxe2ZwhrSTy313zLD+oj8nYFJYy1XH3Lqk3C1Qt4MIPcrLMBXWDTLQYX/3Nh1ip/zVmQN8 VeiAwhDw8q1YV+JaES72wRM1EMRqHjhmC2izjUynSt6y8jXlCHI3enmcwIKf2BRQ2w3x17qL ZK5jpYaGlCvdwUynwaN6kPzxqwdr6N6ZTq2Iw8Ab23tImduX7Hl/LOEb9RC6dUo9z1QSOmna k2yRbv0oh9c2CTmVTg7pnhzZ3ShvZP3mAZ/gWSWISNorXbXTsp3wA/W+N3WQfM5MiMufCBjk nGXA1G9O4Ls5tCIj9LYtfj4UWu9V5pVeC2tzIWatSL963c4SRG4mvmynJXgH21YmWfy0dVwW CSOrFDkZZHmzK+nGe1id0hsQlT77oJ2F5p/nY05mJwLkSJC19PFoDxdyDa1bYQT0LmbDjJFX TMRxt/J/AXpkFZuKH6E3cOxV3mQxNdge8jvZ2oX3iwn6MUZQKyQ7bFCgW50ug/i9VOXMaU7x G5Mj6d/uxt4y6kTtQEgzzuQGOUXFEhcZmn3kgiQqsu5tONRbXqudr650Ax/m8qgBfeMuFI5O j6xd5E8ECt39sg6PkjL1Si544foYtTRK9JVrhqMngzLksBaLZswkrwBgi8tagef9TU1jvU2i xBjx8TwtY6LMWhsuqL/GhlAOyb+eusc/zjsieBVmcPcjOXNVt1xXz4MWpXvV/ehFjkf4O/mO wi5Gzo5sn6HGLDbEFzX+AJ8onnICZzuK2CPKSxT04B5XBfEbh864khcTHAgk5U+DAzv2MHxb BIz+GUK/lCh4hpUlrAzal+mAz+Z/lv3LG9zEsTXLQIKvF8eoR2OaorHsLo1R2YBr/jD5ESMM jDJOVoOVDlTHBTCXxe5ZvGv/YWSrbbeXLbvaauWJ+3J87QWVu/Ul831lNI6uW/dbIPXeSAya p9zkktbASImR4KAwWhJE2pP0HuTJ8+D+EXlon0x95/gtqStAEW1vMOOE+cAaIo0vUnn3eHbc bbX3XgcS34Q14tQlyWQmf5PgRhL0XEoL370TvwBrXKfFvuO3PIHSUdKMWUrc5IZp6MkglsXY JCd0IikkOUiyKZyUgYgNxSpjMitYYZiz3iVElTBCQ7LMb2HIWaO2MTreeanTqUWiuxIthq2s DLdEkn5Pz3FmSO7HxaoefpBii2WJnk88Mm0bwptBG7/TdnndgzzMdl5iiczyKE1gXWCPHAVM Dx1eUdA5rOK6iYQjvJ6Em1Hpn1rSIvM0z6e9PXdI40KvOFDBy11k6dD/i1/xecEqi5DQ/Nxl W3Zqdsv61Cqn++TyyZ2BRpDrjEY4eDD9U5mOKjf6txBQSOepENLvTjWUU1b4Yc0WbiN8+hKx 9PClbz+MmJH+tPQpo4HAtTMbdmAKDwnOAboHzjdCE0ESySqPCfRnR848rna+3uLo5w9spWpl oAJT+oRXVo5DP4bTEQjBNsaLYx8QxsrlLeaiIgD4n/0/3yzDI1K+4vKUP6fG6ClMDGCkbxNf AcF25v9JIUXc5TlgglsNgg8k4PNFE7dG9tKp2cyC2186FUI+394QGop3kvjYQ74+34fG8m/m Rsugxd/a+AgnN8Ny1I+J16PvTVp1UdtyJPqhjeedDO3J6C1D9k+48/cuE04M5e9SAFwP1Xad aNMOzLNRrYXhLxlJzkDtQ== IronPort-Data: A9a23:RZO6ma0jEqZwJl5NJvbD5eh3kn2cJEfYwER7XKvMYLTBsI5bp2EDy GsXDz2PP/yINmfxf9AjboW3/RtXscPXzYVrT1Fk3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOH9IQMcacUsxLbVYMpBwJ1FQyw4bVvqYy2YLjW1jV4 ouoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt/pt7 vBXpbWUciokIr/0nqcCDRwGIwgraMWq+JefSZS+mcmazkmDamW1hvsyXQc5OooX/usxCmZLn RAaAGpVP1bT2qTsmeP9FrgEascLdKEHOKsWvH16wDCfDbA+RojOWK7XzdBd1TY0wMtJGJ4yY uJGNGcyM02ZC/FJElM4BrRijvyNvGulXWwIoWCZgqM0yWeGmWSd15C0aIaPEjCQfu1el0Oc4 2bH5HjRGQAfLNXZyDyf83vqiPWnoM/gcIcbFbn97+AzxVPPlyocDxoZUVb9qv684qKjZz5BA 2YI3A80vYEWz2GmUsvFWV6n/nvajjdJDrK8DNYGwA2Kz6PV5SOQCW4FUiNNZbQaWCkeFWxCO rihz4OBONB/jFGGYSnCqerM/FteLQBQfDBSP3ZVJecQy4C7+Nlbs/7Zcjp0/EeIYjDdHDjxx 3WTsnF7ielCy8EM0Kq/8BbMhDfESnn1ouwdtl6/soGNtFsRiGuZi2qAtAmzARFoct/xc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd9qW7xpi77JdsOsFmSwXuF1O5UKVcFh 2eD6WtsCGN7YRNGkIcrOdvqU51ypUQePY28CKGIBjaxXnSBXFbfoHsGib+40Gfqn0wh+ZzTy r/KGftA+U0yUPw9pBLvH7l1+eZynkgWnDqPLbiilkTP+efAORa9FOhdWHPTP7hRxP7V+239r ocPX+PUkE43eLOlPUHqHXs7dgxiwY4TXs2u96S6t4erfmJbJY3WI6SJkON5Jtc8xPw9eyWh1 ijVZ3K0AWHX3RXvQThmoFg6AF82dZog/389IwI2OlOkhyoqbYq1vfUQcpI2ef8s8+k6lax4S PwMesOhBPVTS2Sfq25NM8Wl9IEyJg62gQ+uPja+ZGdtcpNlQTvP8IC2cwbq8h4IESfq59A1p Ket11+ATJdaH1ZiAc/aZeiB1VS0uXRByut+U1GZcNZWcUTotoNtLnWp3PMwJsgNLzTFxyebh 17GW0dG+bGVrtZsotfThK2Co4O4KMdEHxJXTzvB8LK7FSjG5W78k4JNVeC/ezqCBm75/aOVY /oMk6PxPfgBq1Z9s4RmFoFtw69jtcDkoKVXz1g9EXjGMwarB7dnLiXU1MVDrPcWlLpQuA/zQ 1zWv9cGaPOGP8TqFFNXLw0gN7zR2fYRkzjUzPI0PESqu3MtreTfCR1fb0uWlShQDLppK4d5k +0vj8gbtl6kgR0wP9fa0y1ZqzaWInobX/l1v50WGtWw2A8iy1UHeIKFTyGqsdeAbNJDNkRsK TiR3fKQi7NZz0vEUnwyCXmdgrYH1MpW4EhHnA0YOlCEutvZnftrjhdfxjI6E1ZOxRJd3uMvZ 2VmOiWZ/0lVE+uEWSSCY4ytJ+2FLBiQ+0i00kVQ0WOFHg+nUWvCKGB7MuGIlKzcH6SwYRADl Ix0Ck68OdopQC019iQ3UE9h7ffkSLSdMyXczdu/EZ3t84YSOFLYb2zHWYbMgxTiCMI1wkbAo IGGOQq2hbLTbUYtnkHwN2VWOXn8hvxJyKyujMyNJJ80IFw= IronPort-HdrOrdr: A9a23:AWOpQqF/kXrnXjrrpLqEJseALOsnbusQ8zAXPidKKCC9E/b3qy nKpp8mPHDP6Ar5NEtQ+uxofZPwJU80lqQb3WByB8baYOCOggLBRuwP0WKh+UyGJ8SUzJ856U 4PSdkdNDS9NykdsS+s2njCL/8QhP+d8K6pgu/Cz3BiCT1LRshbnn1E4lbyKDwPeCB2QaY/FI Wd6o55pyG9YzAsZMy9b0N1ItT+mw== X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.90,151,1643670000"; d="scan'208";a="7555711" X-MGA-submission: =?us-ascii?q?MDG8+1hzvLa/YM8fo5MfyQmjI67a7AyMu7tudx?= =?us-ascii?q?IUXYrmWZebdE9zeFzDv7gXfyvXtlQHt8FwJfKte3mAQNzPL7Wk7rwrpy?= =?us-ascii?q?oyqmLIL9ZYGeBdrOfnAe+SUcXq65Stu7mte2ImO8jK6AHc71b9W2fCDu?= =?us-ascii?q?Cjfrq3+5LB19vv8IJXgHCILQ=3D=3D?= Received: from mail-qv1-f49.google.com ([209.85.219.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 03 Mar 2022 20:05:57 +0100 Received: by mail-qv1-f49.google.com with SMTP id j5so4850380qvs.13 for ; Thu, 03 Mar 2022 11:05:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:from:date:message-id:subject:to; bh=uuDfwmi44Atbun+IXyUg0Vf9fEGQfWiLCmEqMeBitL4=; b=XyDc0k+wsXhVX1YJQ1m8GO986hIcret/Zzs9fez2ucLu8HW1jCk4l6SqkbDRfR8JuU 8ku1FNijDve5G0M15QrqdSg5rp/HIClHynTTiL4mXM/LJEgouuZtaKQBXUa9HtIdgmfa guNgBXZR0vM61r9UXp0nteg5m07YCqs0L2gIRuUqs230lLMn0cEx2iiX6k3tMlhAA603 MjCtcqLH6LecDuw3gMzbslVwI8Px+4gHV2X/Ao+DyUHSlYamb1NTbgmTTuJFL1e2dRjA +Ylh7Y95kAXDzR4muu8uAHFrHQ6R+T4JBLONyK9+MubhZyd6ArIFF/Fm/bRdNFAE3qD5 eKsQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=uuDfwmi44Atbun+IXyUg0Vf9fEGQfWiLCmEqMeBitL4=; b=nfv+S9lqUAU6jZGoUDixlK6wXDsNaJPR4E5xQe9cgl3x5erFphydk7OzAYg7B/Be0A GoqYnXt8BWtYq2caqt1hl1GmIgTNNs91FHKKD6V0eGHHl5lGo8cEr2eYQGL69NZQSuDW PR8HXB+c/P/HTotzuO7lPZ2ZnqCS/l1QnAwtb6RwSWQY3eeMN9cQ0d7DJZ8CU3ucfOpU 1mBbCMO1la/I61wMBHx1kStbNMVlNvbI9L+b2KE2fwJFz8LImIzjCYVwKvFxZPiYer36 JMwJ45R6+FwdkqFmy/pw8bDymGuPQXn4Uk+61rh+mBhlsPySCNrPfD4or87k0EC+CjJ+ MAhg== X-Gm-Message-State: AOAM532kunYcseZIJZtrdQ8ttxGhI4pGQkUON72IPH6TVUW4o0an1rf5 O3yK8Z36zRqqwcNopNy6W5ieffOZGxoExYBwbv0= X-Google-Smtp-Source: ABdhPJySY4w0zQpXFXSz4lhOJYGWMqMm6S02JotmzSu5m8zlEHVRfKyV597UvB3i3RwfCgHfsBBRvWOH95AJjPDXzw4= X-Received: by 2002:ad4:5ba1:0:b0:432:a02c:24c9 with SMTP id 1-20020ad45ba1000000b00432a02c24c9mr24851245qvq.8.1646334354729; Thu, 03 Mar 2022 11:05:54 -0800 (PST) MIME-Version: 1.0 From: Andrei Popescu Date: Thu, 3 Mar 2022 19:05:44 +0000 Message-ID: To: acl2@utlists.utexas.edu, agda@lists.chalmers.se, appsem@lists.tcs.ifi.lmu.de, ats-lang-users@googlegroups.com, caml-list@inria.fr Content-Type: text/plain; charset="UTF-8" Subject: [Caml-list] PhD Position in Number Theory and Formalization Reply-To: Andrei Popescu X-Loop: caml-list@inria.fr X-Sequence: 18712 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-funded, 4-year PhD position in Number Theory and Formalization. The preferred starting date is in the period 1 May - 1 September 2022. The candidate will conduct research on Sander Dahmen's NWO-funded project "Formalizing Diophantine algorithms". This amounts to both developing and formalizing (with a proof assistant such as Lean or Coq) number theory necessary for solving Diophantine problems. The focus will be on effective/algorithmic number theory, but more "pure" results will (necessarily) also play an important role. We note that in this project most of the time will likely be spent on actual formalization work and that the proof assistant to be used will probably be Lean (but that is open for discussion). The position also contains a small teaching component. The research will be embedded in the Algebra and Number Theory group of the Mathematics Department and in particular connects to the CAN-endowed chair "Automated verification of mathematical proof" held by Assia Mahboubi. Within the Faculty of Science there will also be close collaboration with (Theoretical) Computer Science, especially the group of Jasmin Blanchette. Applications from all groups currently under-represented in academic posts are particularly encouraged. We are working to improve the present gender balance within the department, and particularly welcome applications from women. More details at https://workingat.vu.nl/ad/phd-position-number-theory-and-formalization/70lg5t