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 ( Sémagramme is a team with a longstanding experience on type theory, 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 candidate will study the logical and linguistic structure of mathematical proofs as they appear in textbooks and scie...