From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10701 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: "Joost J. Joosten" Newsgroups: gmane.science.mathematics.categories Subject: PhD student position on proof theory and verification of legal software, Barcelona Date: Mon, 21 Mar 2022 22:24:08 +0100 Message-ID: Reply-To: "Joost J. Joosten" 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="19447"; mail-complaints-to="usenet@ciao.gmane.io" To: Original-X-From: majordomo@rr.mta.ca Wed Mar 23 19:45:57 2022 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1nX5zZ-0004nt-3G for gsmc-categories@m.gmane-mx.org; Wed, 23 Mar 2022 19:45:57 +0100 Original-Received: from rr.mta.ca ([198.164.44.159]:55592) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1nX5xe-0002y1-5m; Wed, 23 Mar 2022 15:43:58 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1nX5x1-0002Dy-JW for categories-list@rr.mta.ca; Wed, 23 Mar 2022 15:43:19 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10701 Archived-At: PhD student position on proof theory and verification of legal software, Ba= rcelona, Deadline: April 3th, 2022 (AoE) The University of Barcelona offers a 3 year PhD position in collaboration w= ith the Catalan industrial sector. The industrial component of the PhD revo= lves around the development and verification of legal software in Coq withi= n Formal Vindications SL (formalvindications.com). This work will be complemented with the formalisation of parts of l= ogic/mathematics and possibly research of a less applied nature. As such, there are two possible tracks: (1) The PhD student proposes an external supervisor with whom to work on ac= ademic Coq-related questions (such as verified extraction, or others); (2) The PhD student works under the supervision of Joost J. Joosten (joostj= joosten.nl) in the area of proof theory and forma= l logic for the academic part of the thesis. Gross salary is about 22K=E2=82=AC per year (well above average for a PhD s= tudent in Spain) and comes with a travel allowance of at least 2200=E2=82= =AC per year. Starting date should be around August/September 2022. The successful candidate will enter an active and strong logic group in Bar= celona. They will be trained on Coq and functional programming in OCaml by = an experienced team. If needed, the contract can be extended after the init= ial three years. We are looking for very strong candidates with a background in theoretical = computer science, mathematics and/or mathematical logic. It is a strict req= uirement to have finished a relevant Master degree with an average undergra= duate and master score of at least 6.5 out of 10. Interested candidates should send their CV, letter of motivation and academ= ic track record to Aleix Sol=C3=A9 >. Further questions on the position can be sent to Joost J. Joosten >. Joost J. Joosten University of Barcelona C. Montalegre 6 08001 Barcelona, Catalonia, Spain Office phone: +34 9340 37984 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]