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=3.8 required=5.0 tests=DATE_IN_PAST_96_XX, DKIM_ADSP_CUSTOM_MED,FORGED_GMAIL_RCVD,FREEMAIL_FROM, LOCALPART_IN_SUBJECT,RCVD_IN_MSPIKE_H2,SPOOFED_FREEMAIL, SPOOF_GMAIL_MID autolearn=no autolearn_force=no version=3.4.4 Received: (qmail 402 invoked from network); 14 Mar 2023 02:07:31 -0000 Received: from smtp2.mta.ca (198.164.44.75) by inbox.vuxu.org with ESMTPUTF8; 14 Mar 2023 02:07:31 -0000 Received: from rr.mta.ca ([198.164.44.159]:43938) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1pbu3C-0005mN-3t; Mon, 13 Mar 2023 23:06:06 -0300 Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1pbu2m-00026u-Il for categories-list@rr.mta.ca; Mon, 13 Mar 2023 23:05:40 -0300 MIME-Version: 1.0 From: Andrei Popescu Date: Fri, 10 Mar 2023 00:07:38 +0000 Subject: categories: PhD or Postdoc Position at LMU Munich about Verified Modal Logics To: categories@mta.ca Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Precedence: bulk Reply-To: Andrei Popescu Message-Id: We are looking for a PhD student (4 years) or postdoctoral researcher (3 years) to work on the Isabelle formalization of modal model theory. The work will take place within the Chair of Theoretical Computer Science at LMU Munich under Jasmin Blanchette's supervision with the participation of two external experts: Cl=C3=A1udia Nalon (University of Bras=C3=ADlia) and Sophie Tourret (Inria Nancy). Modal logics are extensions of classical logics with operators that allow for the qualification of truth. Model theory for modal logics is concerned with the interplay between the language (syntax, i.e., the set of its formulas) and its meaning (semantics, i.e., the structures over which the language is interpreted). There are, however, different ways of characterizing meaning for modal sentences and also several (well-established) results that allow for restriction on the sets of structures being considered. This project concerns the formalization in Isabelle of those results for general Kripke structures for generalized modal operators (i.e., of any arity). The goal is to produce a library that could then be used (and possibly extended) for specific applications, in particular those related to proof theory. The position is categorized as TV-L E13 according to the German salary scale. It includes some teaching obligations. The starting date is flexible. Please contact Jasmin Blanchette (jasmin.blanchette@ifi.lmu.de) for more information or if you want to apply. The application deadline is 15 April 2023. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]