Contexte et atouts du poste
The 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) :
Avantages
Rémunération
Monthly gross salary amounting to 2788 euros