PhD or Postdoc Position at LMU Munich about Verified Modal Logics

[Andrei Popescu]

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áudia Nalon (University of
Brasília) 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 at ifi.lmu.de) for more information or if you want to
apply. The application deadline is 15 April 2023.