Post-Doctoral Research Visit F - M Formal Proofs In Semigroup Theory H/F INRIA

Post-Doctoral Research Visit F/M Formal proofs in semigroup theory
Le descriptif de l'offre ci-dessous est en Anglais
Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

A propos du centre ou de la direction fonctionnelle

The Inria Rennes - Bretagne Atlantique Centre is one of Inria's eight centres and has more than thirty research teams. The Inria Center is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

Contexte et atouts du poste

The(Fast and Reliable Symbolic Computation) ERC Project aims at delivering instruments for producing computer-aided mathematics with the highest possible guarantee on the correctness of the resulting proofs.

This postdoctoal position is concern with investigating concrete and realistic use cases of computer-aided mathematics, in computational semigroup theory. It is located in the Nantes site of the project, within the Gallinette Inria team. Regular visite to the other site of the project (in Lyon, France) are planned and funded by the project.

Mission confiée

Objectives

The research program involves three axes:

Formally verified combinatorics. A pre-requisite for this project is to expand the available corpus of formally verified combinatorial algebra. We will start from the CoqCombi library [6], which is the state of the art in formalized combinatorics, and enrich it with both proofs of classical results and verified algorithms, first focussing on the algorithms per se, described in pseudo-code-like form, and not on actual implementations.

Verified symbolic computation in Rocq. Verified implementations of the later algorithms, meant to be executed, will possibly combine various approaches to code-generation. We will investigate which combination works best, basing on the recent progress in code extraction, verified compilation but also possibly extending the trusted base of code.

Reliable automated reasoning in semigroup theory. Two approaches actually exist for verifying the outcome of automated methods in semigroup theory. The first one consists in verifying the code that produces this outcome, which endows all results produced by a verified code with the same guarantee of correctness. A second strategy consists, when possible, in verifying the result without relying on the way it was produced, possibly relying on an extra piece of data called a certificate. This project actually involves developing new algorithmic methods in semigroup theory, paying a particular attention to the benefits of a certificate-based approach. We expect to connect with more generic algorithms in rewriting theory, and in particular with their formal verification [5].

Collaboration
The recruited person will be in connection with the other site of the project, as well as with its close collaborators such as the Graphs, Algorithmics and Combinatorics team of the LISN (PAris-Saclay University)

Principales activités

Main activities (5 maximum) :

- Conduct fundamental research
- Communicate on advances and results by delivering scientific talks and submitting research papers

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

Rémunération

Monthly gross salary amounting to 2788 euros