PhD Position F/M Advanced elaboration techniques in proof assistants

The Malinca project (ERC Synergy, http://malinca.org), with centers in Paris, Nancy, Nice and Madrid, aims to develop a new generation of proof assistant technologies capable of understanding the dynamic linguistic structures found in current high-level mathematical texts. The project includes the study of interpretation mechanisms for logical foundations, a new linguistic layer representing the intermediate steps between natural language texts and formalised proof documents, and automation tools for the efficient construction of definitions, theorems and proofs. In application we aim to make the use of computational formalization for mathematical research writing practical and commonplace.

Proof assistants are softwares which allow to formalise mathematical statements and to semi-interactively develop proofs of these statements. Over the last 30 years a larger and larger number of techniques, known as elaboration techniques, have been developed to make the formalisations closer to how mathematicians communicate proofs between themselves.

A key technique of elaboration is unification which supports basic inference of implicit information (e.g. how to infer the domain of an operation), pattern recognition (e.g. how to recognise the pattern of an associativity property in a statement), proof automation (e.g. how to chain lemmas exposing specific properties). Virtually, unification could actually support more advanced levels of inference. For instance, patterns could be unified up to some decidable theories (e.g. modulo associativity and commutativity, e.g. [1]), or up to classes of isomorphisms (e.g. we may want to identify the two standard mathematical implementations of natural numbers, with 0 and +1, or
with binary digits [2]). The question of when a unique solution exists or when heuristics are worth to be applied is also an important question. For instance, new advanced classes of unification problems with unique solutions have recently been studied [3]. The question of how to intertwine the deterministic part of unification and the heuristical part is also a difficult algorithmic question.

The objective of the PhD will be to study the different facets of unification in the context of a type-theory based proof assistant, keeping in mind to produce reusable research results as well as efficient algorithms making proof assistants closer to what mathematical users expect from them.

[1] Alexandre Boudet, Evelyne Contejean, "AC-Unification of Higher-Order Patterns", 1997
[2] Cyril Cohen, Enzo Crance, Assia Mahboubi, "Trocq: Proof Transfer for Free, With or Without Univalence", 2024.
[3] Tomer Libal, Dale Miller, "Functions-as-constructors higher-order unification: extended pattern unification", 2022.

Background in type theory, semantics of computation, proof assistants, algorithmic, unification techniques, formalisation recommended.

Fluency in French or English recommended.

• 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 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