Post-Doctoral Research Visit F/M Formalization/Informalization of mathematical proofs

Télécharger l'offre au format PDF
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

Contexte et atouts du poste

The Sémagramme team at Inria Nancy is looking for a post-doc candidate with a strong background in formal methods, in particular in type theories, proof assistants and logical frameworks. The post-doc will join the MALINCA project (https://malinca.gitlabpages.inria.fr/malinca.gitlab.io/team/). Sémagramme is a team with a longstanding experience on formal methods, logic and computational linguistic.

Mission confiée

The main objective of the Malinca project is to bridge the linguistic gap between the way mathematicians express pieces of mathematics and the way these same pieces are fully formalized using proof-assistants.  In particular, the Malinca project aims to propose new ways of formally expressing mathematical proofs that closely resemble how mathematicians naturally write them. The subject of the postdoc is in line with this objective. The postdoctoral researcher will conduct experiments on the formalization and informalization of mathematical proofs.  To this end, the candidate will take advantage of a system based on the grammatical framework GF and the logical framework Dedukti, developed by Aarne Ranta in the context of the Informath project (https://github.com/GrammaticalFramework/informath).  

Principales activités

  • Study of the linguistic and discursive structure of proofs ;
  • Development of grammars for proof generation ;
  • Development of grammars for proof parsing ;
  • Participation to the design of the Malinca language.

Compétences

  • Solid background in software development and formal methods
  • Familiarity with Dedukti and/or GF is a plus
  • Good writing skills in English

Avantages

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Rémunération

€2788 gross/month