Research and Development Engineer (M/F), the Capla Programming Language

The Inria Saclay-Île-de-France Research Centre was established in 2008. It has developed as part of the Saclay site in partnership with Paris-Saclay University and with the Institut Polytechnique de Paris .

The centre has 40 project teams , 27 of which operate jointly with Paris-Saclay University and the Institut Polytechnique de Paris; Its activities occupy over 600 people, scientists and research and innovation support staff, including 44 different nationalities.

One of the long-term goals of the ERC project Fresco1 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,2 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. There is also an ongoing postdoc work that
makes it possible to invoke Capla code from the Rocq prover and to
carry over the semantics of this code to Rocq proofs.

Now that the project has shown its meaningfulness, it is important to ensure that the lan-
guage and the compiler are both widely usable and sufficiently robust to last.

The work will be carried out mainly in the Toccata team location in
Gif-sur-Yvette and partly in the partner company offices in
Paris. Travel expenses are covered within the limits of the scale in
force.

The primary objective of this position is to improve the language and the compiler with features
that might blocking for a wider adoption:

1. Add support for records (i.e., C struct) to the language, as only arrays are currently
supported. While adding record types does not pose any difficulty as far as the theory is
concerned, it will require some tedious work to adapt the formal proofs of the compiler
and of the type safety, especially if the splitting constructs from the language are extended
to support records.
\
2. Add support for function calls inside size expressions. Currently, only simple expressions
are allowed to describe the size of an array; it is not possible to invoke functions (e.g., the
absolute value). This work item is expected to be difficult and long, as it will require some
large changes to the semantics and the compiler, and therefore to the formal proof.
A secondary objective is to improve the Rocq formalization to make it more maintainable in
the long run:

3. Disentangle the type safety from the type checker. Currently, both are proved at once,
which means that improving the type checker would break the type safety of the language.

This work item requires to design some algorithm-free typing rules and to split the existing
formal proof accordingly. It should be rather simple.

4. Close the gap between the small-step semantics and the big-step semantics of Capla. The
former is used for the proofs of type safety and compiler correctness, while the latter is used
to prove the specification of Capla programs. But the formal relation between them has
been proved in only one direction, which means that, while unlikely, the big-step semantics
could be vacuously correct by accident, and thus the Capla programs would be too. This
work item is purely at the semantics level and does not touch the compiler. It is unclear
how difficult it is.

If time permits or if some of the previous items end up being unreachable, a last objective
is to improve the interface with the Rocq proof assistant:

5. Make it simpler to import Capla code inside Rocq to prove its correctness. Currently,
the process involves passing a debug option to the compiler and moving some Rocq files
around. Ideally, it should be possible to directly invoke the compiler from a Rocq session.
This work item does not involve the semantics and the formal proofs, but it might be
require touching the implementation of Rocq.

Software development in Rocq, development of
specifications and proofs, software experimentation, writing
documentation, contribution to the writing of scientific articles.

Knowledge about the semantics of programming languages and their
implementation is required.  Knowledge of the Rocq proof assistant or
of a closely-related formal system (e.g., Lean), is
required. 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 (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
• Social security coverage

In regards to professional experiences