Temporary scientific engineer / Software engineering / Algorithmics, Computer Algebra, Verification / Graduate degree or equivalent F/M

The Inria research centre in Lyon (previously the Lyon branch of the Inria centre in Grenoble) is the 9th Inria research centre, formally created in December 2021.  It brings together approximately 270 people (including 110 Inria employees) in 15 research teams and research support services.

Its staff are distributed at this stage on 2 campuses: in Villeurbanne La Doua (Centre / INSA Lyon / UCBL) on the one hand, and Lyon Gerland  (ENS de Lyon) on the other. A third site should be opened in the course of 2022. The teams are mainly hosted with our partners.  The centre's teams work closely with research and higher education institutions (ENS de Lyon, UCBL, INSA Lyon, etc.), their laboratories, and other research organisations in Lyon (CNRS, INRAE, competitiveness clusters, etc.), but also with Lyon and regional economic players. Many international collaborations are also underway.

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.

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 implement and formally verify well-known libraries such as GMP or BLAS/LAPACK. 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. But to turn the Rocq proof assistant into a usable computer algebra system, one should also be able to define such Capla functions inside a Rocq script. Moreover, the user experience should be improved by having better runtime error reporting as well as debugging features.

This position 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. The position will last up to 24 months or until the end of the Fresco project (currently set to end on 2026-10-31), whichever comes first. The starting date is negotiable.

The overall objective of this engineer position is to improve the user experience of the Capla language and its compiler, especially when used in conjunction with the Rocq proof assistant, and to exercise it on several use cases.

The recruited person will work in collaboration with Guillaume Melquiond, a senior researcher at Inria.

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:

• offer some syntax highlighting and improve error reporting;
• offer 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.

Finally, to exercise the language and the environment around it, the third objective is to implement some Capla libraries (but not formally prove them, unless the engineer comes with a suitable background) that would be useful in the setting of a computer algebra system. Some potential targets are

• arbitrary precision integer arithmetic,
• algebraic structures over specific finite fields,
• preconditioners/oracles for reliable numerical computations.

Knowledge of the OCaml programming language or a related language is mandatory. Knowledge of the inner workings of compilers is recommended. Knowledge of the Rocq proof assistant is not required, but it would be very valuable. Knowledge of French is not required.

• 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
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Complementary health insurance under conditions

From 2,692 € (depending on experience and qualifications).