---------- Forwarded message --------- Two PhD positions funded by the ANR projects BLaSST and ICSPA on subjects around formal proofs for set-based specification languages are available at Inria Nancy.
Automated Reasoning for Set Theory (Stephan Merz, Sophie Tourret) https://jobs.inria.fr/public/classic/fr/offres/2022-04898 The main objective is to take advantage of recent progress in automated reasoning for fragments of higher-order logic, and to further contribute to them, specifically for proof obligations generated by the B method. Formalization of Set Theory and Proof Checking (Stephan Merz, Gilles Dowek) https://jobs.inria.fr/public/classic/fr/offres/2022-04909 The thesis will study encoding the set theory of the specification language TLA+ in Dedukti, with the objectives of checking proofs obtained by the TLA+ proof system TLAPS, as well as of enabling interoperability with specifications written in the B language. More details on the two subjects, as well as information about how to apply, are available at the URLs indicated above. The theses are meant to start in the fall of 2022, the exact starting date is negotiable. I will be very happy to answer any question about the two thesis offers. Stephan Merz -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logica-l@dimap.ufrn.br> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LitE2Vj6f_%2BTFXUT6%3DsjcRk6Ppa73Z9cHhbMfUvrX0-%2BA%40mail.gmail.com.
