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 45FCC5D5 for ; Wed, 26 May 2021 13:13:57 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.82,331,1613430000"; d="scan'208";a="510069111" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 26 May 2021 15:13:54 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 37813E03B5; Wed, 26 May 2021 15:13:54 +0200 (CEST) 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 16167E03B5; Wed, 26 May 2021 15:13:48 +0200 (CEST) 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-qk1-f174.google.com IronPort-PHdr: =?us-ascii?q?A9a23=3ARtoAhhfU7InWAHI5xOJkd6pwlGM+7tnLVj580XL?= =?us-ascii?q?Ho4xHfqnrxZn+JkuXvawr0AaYG9+Lsbka0qL/iOPJYSQ4+5GPsXQPItRndiQur?= =?us-ascii?q?oEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZ?= =?us-ascii?q?vJuTyB4Xek9m72/q99pHOZwhEniSxbLBsIBm5rAjdq9QdjJd/JKo21hbHuGZDd?= =?us-ascii?q?f5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgX?= =?us-ascii?q?MTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KhsVRHoj?= =?us-ascii?q?z0HNyIn/27KlsJ/kr5UoBO5pxBh3oXYZI6YOOZ7cq7bYNgUR3dOXtxJWiNOAo2?= =?us-ascii?q?yYYgBAfcfM+lEoIfwvEcOrQKkCAWwGO/j1j1Fi3nr1qM6yeQhFgTG0RQ8EtIIr?= =?us-ascii?q?XvUtsv6NKYPWu6vy6nI1SvMb+hK1jfg9YPFdQouofeRUrJqb8XRyFMjFwPfglW?= =?us-ascii?q?IrozlJy2a1v8RvGiG9OdgWuevhHQmqwF1uDSg2sAsiozQi48T11vL+jl3zpwvK?= =?us-ascii?q?t2kVE50f8SkEJ1Iui2HNoZ7TcAvT392tCskzrAIt5q2cTUXxZg7xhPSZPOKfYi?= =?us-ascii?q?G7x/tVOucPzl1iXJ7db+iiRu/7Eitx+7/W8e00FtHqDdOnNfLtnAIzRPT686HR?= =?us-ascii?q?+Nj/ke8wzqP0QTT5+dZKk43jarWM4AtzqI0m5YJsknOHjX6lFvogKOIbEko5+q?= =?us-ascii?q?l5uvhb777vJGTLZV0hRv7Mqk2msywH+A4Mg8WUmie4+u81bnj8VTgQLVJk/E6i?= =?us-ascii?q?6fZvI3YKMkUvKK5DAhV0oEs6xa7ETiqysgXnX4CLF5deRKHiZbmO03WLfzmEfu?= =?us-ascii?q?yh06gnTRryvzcILHtHIvBImLenLrjcrtx80tcxxAyzdBb6ZJUELYBIPfrV0Drs?= =?us-ascii?q?tzXEwU5PBK1w+r9CNVxzJseWWWXAqCHK6PdrUKI6/kgI+mJfoAVuTL9J+I56P7?= =?us-ascii?q?piH81gUUdcrWx3ZsLdHC4GexrLFmDbnrphtcNCGMKvgslTOz2k1CCSj5SZ3OqX?= =?us-ascii?q?60m/D07CYSmDZ3CRo+3mrCB0j27FIVMZm9aElCMDWvod4KcVvgQbyKSO9ZtnSA?= =?us-ascii?q?AVbi8UIAszgqutQ//y7p/NOXY4CwYtZT51Nh0/eLfjx8y9SYnR/iahmqESmUxm?= =?us-ascii?q?mITWxc32rp+qApz0BPL2qFkjvNfD91e/NtMTg58PpeYh+d9EpX5Xh/LVtaPUle?= =?us-ascii?q?vBNu8RXk9Svo9x5kNeQB6AdrxoArE2n+DBbMPmr3DPJss/7nXwjClLsBx0XvHk?= =?us-ascii?q?qlnl14+T9BEKEWpg6d+807YAIufwBbRrLqjaalJhH2Fz2yE12fb4BkwuOFYXqD?= =?us-ascii?q?MXHRZbUzT/42RDqLqSravDfE+MVIEx5fddu1FbdrmiVgAT/Dmaoy2i4eZlGK5B?= =?us-ascii?q?BLOzbSJPtKCRg=3D=3D?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3A/FPM/K3xs6ZjimtUPU0+pQqjBLEkLtp133Aq?= =?us-ascii?q?2lEZdPUzSL3/qynOpoV96faQslwssR4b6LO90cW7IU80lqQV3WByB8bBYOCOgg?= =?us-ascii?q?LBR72KhrGSpgEIdReOktK1Fp0NT0G9MrDN5JRB4voSKTPXL+od?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AxAAD2SK5gf67eVdFaFgYBAQEBAQEHA?= =?us-ascii?q?QESAQEEBAEBQIFEBgEBCwGDIVY7MYRIkAKDFIovhVoFigKBfAsBAwENNQwEAQG?= =?us-ascii?q?GUAIdBwEEMQgOAgQVAQEFAQEBAgEDAwQBEwEBDQsLCCcchWgNgjgMGoN/ER0BG?= =?us-ascii?q?x4DEhAPAiYCJAERAQUBIzSCUIJUAQMvD5p/gQQ9izKBFQUBF4EBgggGhQYKGSg?= =?us-ascii?q?NYwOBVgIBBhJ+KgGFaYEfgkcfhCCBBIElgUuGDAOEdoJkBIN/AoERvTQHgxqBL?= =?us-ascii?q?Jw0KYNLAaIGkB2FI6Q1ECMSgSECghAzGiOBAYI4UBkOjh+DcIRwhW9DLwI2AgY?= =?us-ascii?q?BCQEBAwkBiW0BAQ?= X-IPAS-Result: =?us-ascii?q?A0AxAAD2SK5gf67eVdFaFgYBAQEBAQEHAQESAQEEBAEBQIF?= =?us-ascii?q?EBgEBCwGDIVY7MYRIkAKDFIovhVoFigKBfAsBAwENNQwEAQGGUAIdBwEEMQgOA?= =?us-ascii?q?gQVAQEFAQEBAgEDAwQBEwEBDQsLCCcchWgNgjgMGoN/ER0BGx4DEhAPAiYCJAE?= =?us-ascii?q?RAQUBIzSCUIJUAQMvD5p/gQQ9izKBFQUBF4EBgggGhQYKGSgNYwOBVgIBBhJ+K?= =?us-ascii?q?gGFaYEfgkcfhCCBBIElgUuGDAOEdoJkBIN/AoERvTQHgxqBLJw0KYNLAaIGkB2?= =?us-ascii?q?FI6Q1ECMSgSECghAzGiOBAYI4UBkOjh+DcIRwhW9DLwI2AgYBCQEBAwkBiW0BA?= =?us-ascii?q?Q?= X-IronPort-AV: E=Sophos;i="5.82,331,1613430000"; d="scan'208";a="382522638" X-MGA-submission: =?us-ascii?q?MDEOtkn6zSTtiPNCucidb+qTv5WVUqASFdZx4k?= =?us-ascii?q?lNeUIH3LVZ9pR/zA5i8dH/0cJvfMgPo/3el3TUH1vbt9URgwSXvvfkvE?= =?us-ascii?q?Bj99sJm183yee0D360+0kf111Bx9r6BsKpQhYtsR30h1eerqdYRCs6NL?= =?us-ascii?q?b1OCjy8ycDohpjtEweYB7+TQ=3D=3D?= Received: from mail-qk1-f174.google.com ([209.85.222.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 26 May 2021 15:13:44 +0200 Received: by mail-qk1-f174.google.com with SMTP id 76so839608qkn.13; Wed, 26 May 2021 06:13:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=feZjj3DVKOdX4YOOx+djyIrtAJFy3HNOsE6ZppIZI/M=; b=RI7+cBfLsWzwmsfjDy5fqNh/icRsYLySYn4ScCXC7qUrpNtFkC40AI/duaArNR+gAs jB1qJHnuigfRgX8CSYW0mTtHyXmudOebhuwJCIlZY9j6AoKMkBG8Fx0jIXRsdbtYdNs8 PRIPzHArua4k9IChiRxJjY4WFqw8GzYQqnvqG/OC4pzySoC+UwOz4KMdFoCbRnDCfVDq waAOLkSF9yNJ/DUnovG55z9Pn93sIjO3mTS2gQ5BTW4fG7n8f/dw7oIeUVkwmQUy6wVW ZyYl8ppIAJwGaBBTg+t8De/89FxnRfH/mblzLFRnzlLHp5s8/V8GigsqJlQ+dcUVnGde Mibg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=feZjj3DVKOdX4YOOx+djyIrtAJFy3HNOsE6ZppIZI/M=; b=MkKHu9zHa/yRUqPyeOei6zPoukVj/plOmTZA2ZNrOloEoxlbo/Y0+jq9VNufo0L6fA DyafPAkQBRAGD2lvLWSHd8pyWESBT7PEDgXkgam7+XDxLobcJqTc9dFdzbDMnueHfY8v VKv9NKyGEF9Sp5VUEC62TrOp5hDjadDbB3Uv8ZNoshsq3eEnVTWXJvd9hOBMs2HFiEiB duUOQCKHnBoqLpzdX5lFyZzZqzeHVTgqPSnbTAYnJIo2Qzvk8StvGlGsL3w9qi7G855o 26sj+zZc2VPDrSaERd5MsFbT0s0wpfYttQp3hlZeVMCjPmY4v2Yo5/czLn7W/Hls4JDh nFpw== X-Gm-Message-State: AOAM532bNxOzcQ/FSa8rfXOO1OQajsU+BqzayMPKKVkahI75W6doZ3mK lJsUbP4MLqB0cAqqgJ0G3Xub6Md/vWzssQJ249aajJebNdKOZw== X-Google-Smtp-Source: ABdhPJwm6IZqugqqK9eBaaPBhDxzpjuez2KNO5iaMwjNRct4jVGl1Gowmq4Xho/+F1zJMc2EOtR2pKY9VvhFXvMb4TA= X-Received: by 2002:a37:6496:: with SMTP id y144mr40418069qkb.147.1622034823368; Wed, 26 May 2021 06:13:43 -0700 (PDT) MIME-Version: 1.0 From: Andrei Popescu Date: Wed, 26 May 2021 14:13:32 +0100 Message-ID: To: caml-list@inria.fr, categories@mta.ca, coq-club@inria.fr, dl@dl.kr.org Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: [Caml-list] PhD position on the formalization of logical calculi in =?UTF-8?Q?Saarbr=C3=BCcken?= Reply-To: Andrei Popescu X-Loop: caml-list@inria.fr X-Sequence: 18506 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: A PhD position is open at the MPI for Informatics in Saarbr=C3=BCcken, supervised by Christoph Weidenbach, Jasmin Blanchette and Sophie Tourret. The project is about using Isabelle/HOL to formalize logical calculi. See https://www.cs.vu.nl/~jbe248/sb_job.html for more information.