Publiée 4 juin 2026
Temporary scientific engineer / Bridging the gap between the Rocq proof assistant and computer algebra libraries / Proofs and Verification / Graduate degree or equivalent
Inria
Lyon, Auvergne-Rhône-Alpes 69061 CEDEX 06, France
CDI
A propos du centre ou de la direction fonctionnelle
The Inria research centre in Lyon is the 9th Inria research centre, formally created in January 2022. It brings together approximately 410 people in 20 research teams and research support services.
Its staff are distributed in Villeurbanne, Lyon Gerland, and Saint-Etienne.
The Lyon centre is active in the fields of software, distributed and high-performance computing, embedded systems, quantum computing and privacy in the digital world, but also in digital health and computational biology.
Contexte et atouts du poste
One of the long-term goals of the ERC project Fresco is to turn the Rocq proof assistant into a competitive tool for doing verified computer algebra. In particular, this requires the ability to perform intensive computations in a formally guaranteed way.
A significant milestone was the design of Capla , a safe low-level imperative language suitable for implementing such algorithms, as well as the development of a formally verified compiler for this language. It is now possible to write a library using Capla, to compile it to machine code, to verify its correctness using Rocq, and to invoke its functions from C code.
Another notable improvement was the ability to invoke arbitrary external code during convertibility checks in Rocq's kernel. (To preserve consistency, external code must adhere to some restrictions, e.g., no observable non-determinism.) An example of such external code is the mpz layer of the GNU Multi Precision Arithmetic library, which can be invoked to perform efficient computations on large integers.
Mission confiée
The goal of this work is to improve both the Capla tooling and the ability for Rocq to invoke external code. In particular, the gap between both features should be bridged, that is, it should be possible to execute some verified Capla code seamlessly from a Rocq proof.
Bibliography around Capla :
This work will take place at the LIP Computer Science laboratory of ÉNS Lyon, in the Inria team Pascaline , which aims at advancing the fields of computer arithmetic and computer algebra, with a strong accent on formal verification.
Principales activités
The first objective of this engineer position is to make it possible to write, compile, and dynamically link a Capla function, without having to leave the confines of the proof assistant. This requires to tackle several challenges:
The second objective is to make the use of Capla more effective, both inside and outside the proof system:
The third objective is to widen the set of computer algebra libraries that can be invoked from a Rocq proof:
The first objective requires modifying some code of the Rocq proof assistant, mostly at the level of the user interface. The second objective involves some code of the Capla compiler. In both cases, the primary language is OCaml, with potentially some Rocq code. The third objective involves some C code, as well as the need to express some complicated mathematical specifications in Rocq.
Avantages
Rémunération
From 2692 € gross/month (depending on experience and qualifications)
The Inria research centre in Lyon is the 9th Inria research centre, formally created in January 2022. It brings together approximately 410 people in 20 research teams and research support services.
Its staff are distributed in Villeurbanne, Lyon Gerland, and Saint-Etienne.
The Lyon centre is active in the fields of software, distributed and high-performance computing, embedded systems, quantum computing and privacy in the digital world, but also in digital health and computational biology.
Contexte et atouts du poste
One of the long-term goals of the ERC project Fresco is to turn the Rocq proof assistant into a competitive tool for doing verified computer algebra. In particular, this requires the ability to perform intensive computations in a formally guaranteed way.
A significant milestone was the design of Capla , a safe low-level imperative language suitable for implementing such algorithms, as well as the development of a formally verified compiler for this language. It is now possible to write a library using Capla, to compile it to machine code, to verify its correctness using Rocq, and to invoke its functions from C code.
Another notable improvement was the ability to invoke arbitrary external code during convertibility checks in Rocq's kernel. (To preserve consistency, external code must adhere to some restrictions, e.g., no observable non-determinism.) An example of such external code is the mpz layer of the GNU Multi Precision Arithmetic library, which can be invoked to perform efficient computations on large integers.
Mission confiée
The goal of this work is to improve both the Capla tooling and the ability for Rocq to invoke external code. In particular, the gap between both features should be bridged, that is, it should be possible to execute some verified Capla code seamlessly from a Rocq proof.
Bibliography around Capla :
- Josué Moreau. Programming language and formally verified compiler for low-level numerical libraries. 2025. https://hal.science/tel-05412981
- Guillaume Melquiond, Josué Moreau. A safe low-level language for computer algebra and its formally verified compiler. 2024. https://doi.org/10.1145/3674629
This work will take place at the LIP Computer Science laboratory of ÉNS Lyon, in the Inria team Pascaline , which aims at advancing the fields of computer arithmetic and computer algebra, with a strong accent on formal verification.
Principales activités
The first objective of this engineer position is to make it possible to write, compile, and dynamically link a Capla function, without having to leave the confines of the proof assistant. This requires to tackle several challenges:
- devise a quotation mechanism to embed some Capla code inside a Rocq proof script;
- implement some Rocq commands to invoke the Capla compiler to produce both the compiled code (which is then to be linked it into the proof system) and the Rocq term that represents the source Capla function.
The second objective is to make the use of Capla more effective, both inside and outside the proof system:
- provide some syntax highlighting and improve error reporting;
- produce some basic debugging facilities, especially inside the proof system;
- reduce the distance that might exist between the Capla code, as written by the user, and its abstract syntax tree inside the proof system, as seen by the user when doing a proof.
The third objective is to widen the set of computer algebra libraries that can be invoked from a Rocq proof:
- implement, if possible automatically, the glue needed to invoke the functions of a C library such as FLINT ;
- provide some meaningful Rocq specification for those libraries.
The first objective requires modifying some code of the Rocq proof assistant, mostly at the level of the user interface. The second objective involves some code of the Capla compiler. In both cases, the primary language is OCaml, with potentially some Rocq code. The third objective involves some C code, as well as the need to express some complicated mathematical specifications in Rocq.
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 (90 days / year) and flexible organization of working hours
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
Rémunération
From 2692 € gross/month (depending on experience and qualifications)
