Research and Development Engineer

Le descriptif de l'offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Ingénieur scientifique contractuel

Niveau d'expérience souhaité : Jeune diplômé

A propos du centre ou de la direction fonctionnelle

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.

Contexte et atouts du poste

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.

Mission confiée

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.

1. 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:

1. 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.

Principales activités

Software development in Rocq, development of

specifications and proofs, software experimentation, writing

documentation, contribution to the writing of scientific articles.

Compétences

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.

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
• Social security coverage

Rémunération

In regards to professional experiences

Informations générales

• Thème/Domaine : Preuves et vérification

Ingénierie logicielle (BAP E)
- Ville : Gif-sur-Yvette
- Centre Inria : Centre Inria de Saclay
- Date de prise de fonction souhaitée :
- Durée de contrat : 6 mois
- Date limite pour postuler :

Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.

Consignes pour postuler

Sécurité défense :

Ce poste est susceptible d'être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n° relatif à la protection du potentiel scientifique et technique de la nation (PPST). L'autorisation d'accès à une zone est délivrée par le chef d'établissement, après avis ministériel favorable, tel que défini dans l'arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l'annulation du recrutement.

Politique de recrutement :

Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.

Contacts

• Équipe Inria : TOCCATA
• Recruteur :

Marche Claude /

L'essentiel pour réussir

The candidate will be required to work with Guillaume Melquiond and

also to participate in joint activities of the research team: joint

seminar, working groups, etc.

A propos d'Inria

Inria est l'institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l'interface d'autres disciplines. L'institut fait appel à de nombreux talents dans plus d'une quarantaine de métiers différents. 900 personnels d'appui à la recherche et à l'innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.

---