From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10491 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Andrei Popescu Newsgroups: gmane.comp.lang.caml.inria,gmane.science.mathematics.categories,gmane.science.mathematics.logic.coq.club Subject: PhD position on the formalization of logical calculi in =?UTF-8?Q?Saarbr=C3=BCcken?= Date: Wed, 26 May 2021 14:13:32 +0100 Message-ID: Reply-To: Andrei Popescu Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="17855"; mail-complaints-to="usenet@ciao.gmane.io" To: caml-list@inria.fr, categories@mta.ca, coq-club@inria.fr, dl@dl.kr.org Archived-At: Original-X-From: caml-list-owner@inria.fr Wed May 26 15:13:58 2021 Return-path: Envelope-to: gclci-caml-list@m.gmane-mx.org Original-Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1lltME-0004OE-7h for gclci-caml-list@m.gmane-mx.org; Wed, 26 May 2021 15:13:58 +0200 X-IronPort-AV: E=Sophos;i="5.82,331,1613430000"; d="scan'208";a="510069150" Original-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:55 +0200 Original-Received: by sympa.inria.fr (Postfix, from userid 20132) id C741AE0AF6; Wed, 26 May 2021 15:13:55 +0200 (CEST) Original-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/tVOucPzl1iXJ7d 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?= Original-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 Original-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) X-Loop: caml-list@inria.fr X-Sequence: 18506 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Original-Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: X-Gmane-Expiry: 2021-06-09 Xref: news.gmane.io gmane.comp.lang.caml.inria:69459 gmane.science.mathematics.categories:10491 gmane.science.mathematics.logic.coq.club:23063 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.