<p><br />One of the long-term goals of the ERC project Fresco1 is to turn the<br />Rocq proof assistant into a competitive tool for doing verified<br />computer algebra. In particular, this requires the ability to<br />implement and formally verify well-known libraries such as GMP or<br />BLAS/LAPACK. A significant milestone was the design of Capla,2 a safe<br />low-level imperative language suitable for implementing such<br />algorithms, as well as the development of a formally verified compiler<br />for this language.<br /><br />It is now possible to write a library using Capla, to compile it to<br />machine code, to verify its correctness using Rocq, and to invoke its<br />functions from C code. There is also an ongoing postdoc work that<br />makes it possible to invoke Capla code from the Rocq prover and to<br />carry over the semantics of this code to Rocq proofs.<br /><br />Now that the project has shown its meaningfulness, it is important to ensure that the lan-<br />guage and the compiler are both widely usable and sufficiently robust to last.<br /><br />The work will be carried out mainly in the Toccata team location in<br />Gif-sur-Yvette and partly in the partner company offices in<br />Paris. Travel expenses are covered within the limits of the scale in<br />force.</p>
Mission confié
<p> </p>
<p><br />The primary objective of this position is to improve the language and the compiler with features<br />that might blocking for a wider adoption:<br /><br />1. Add support for records (i.e., C struct) to the language, as only arrays are currently<br />supported. While adding record types does not pose any difficulty as far as the theory is<br />concerned, it will require some tedious work to adapt the formal proofs of the compiler<br />and of the type safety, especially if the splitting constructs from the language are extended<br />to support records.<br />\<br />2. Add support for function calls inside size expressions. Currently, only simple expressions<br />are allowed to describe the size of an array; it is not possible to invoke functions (e.g., the<br />absolute value). This work item is expected to be difficult and long, as it will require some<br />large changes to the semantics and the compiler, and therefore to the formal proof.<br />A secondary objective is to improve the Rocq formalization to make it more maintainable in<br />the long run:<br /><br />3. Disentangle the type safety from the type checker. Currently, both are proved at once,<br />which means that improving the type checker would break the type safety of the language.<br /><br />This work item requires to design some algorithm-free typing rules and to split the existing<br />formal proof accordingly. It should be rather simple.<br /><br />4. Close the gap between the small-step semantics and the big-step semantics of Capla. The<br />former is used for the proofs of type safety and compiler correctness, while the latter is used<br />to prove the specification of Capla programs. But the formal relation between them has<br />been proved in only one direction, which means that, while unlikely, the big-step semantics<br />could be vacuously correct by accident, and thus the Capla programs would be too. This<br />work item is purely at the semantics level and does not touch the compiler. It is unclear<br />how difficult it is.<br /><br />If time permits or if some of the previous items end up being unreachable, a last objective<br />is to improve the interface with the Rocq proof assistant:<br /><br />5. Make it simpler to import Capla code inside Rocq to prove its correctness. Currently,<br />the process involves passing a debug option to the compiler and moving some Rocq files<br />around. Ideally, it should be possible to directly invoke the compiler from a Rocq session.<br />This work item does not involve the semantics and the formal proofs, but it might be<br />require touching the implementation of Rocq.</p>
Principales activités
<p>Software development in Rocq, development of<br />specifications and proofs, software experimentation, writing<br />documentation, contribution to the writing of scientific articles.</p>
Compétences
<p><br />Knowledge about the semantics of programming languages and their<br />implementation is required. Knowledge of the Rocq proof assistant or<br />of a closely-related formal system (e.g., Lean), is<br />required. Knowledge of French is not required.</p>
<p><br />One of the long-term goals of the ERC project Fresco1 is to turn the<br />Rocq proof assistant into a competitive tool for doing verified<br />computer algebra. In particular, this requires the ability to<br />implement and formally verify well-known libraries such as GMP or<br />BLAS/LAPACK. A significant milestone was the design of Capla,2 a safe<br />low-level imperative language suitable for implementing such<br />algorithms, as well as the development of a formally verified compiler<br />for this language.<br /><br />It is now possible to write a library using Capla, to compile it to<br />machine code, to verify its correctness using Rocq, and to invoke its<br />functions from C code. There is also an ongoing postdoc work that<br />makes it possible to invoke Capla code from the Rocq prover and to<br />carry over the semantics of this code to Rocq proofs.<br /><br />Now that the project has shown its meaningfulness, it is important to ensure that the lan-<br />guage and the compiler are both widely usable and sufficiently robust to last.<br /><br />The work will be carried out mainly in the Toccata team location in<br />Gif-sur-Yvette and partly in the partner company offices in<br />Paris. Travel expenses are covered within the limits of the scale in<br />force.</p>
Mission confié
<p> </p>
<p><br />The primary objective of this position is to improve the language and the compiler with features<br />that might blocking for a wider adoption:<br /><br />1. Add support for records (i.e., C struct) to the language, as only arrays are currently<br />supported. While adding record types does not pose any difficulty as far as the theory is<br />concerned, it will require some tedious work to adapt the formal proofs of the compiler<br />and of the type safety, especially if the splitting constructs from the language are extended<br />to support records.<br />\<br />2. Add support for function calls inside size expressions. Currently, only simple expressions<br />are allowed to describe the size of an array; it is not possible to invoke functions (e.g., the<br />absolute value). This work item is expected to be difficult and long, as it will require some<br />large changes to the semantics and the compiler, and therefore to the formal proof.<br />A secondary objective is to improve the Rocq formalization to make it more maintainable in<br />the long run:<br /><br />3. Disentangle the type safety from the type checker. Currently, both are proved at once,<br />which means that improving the type checker would break the type safety of the language.<br /><br />This work item requires to design some algorithm-free typing rules and to split the existing<br />formal proof accordingly. It should be rather simple.<br /><br />4. Close the gap between the small-step semantics and the big-step semantics of Capla. The<br />former is used for the proofs of type safety and compiler correctness, while the latter is used<br />to prove the specification of Capla programs. But the formal relation between them has<br />been proved in only one direction, which means that, while unlikely, the big-step semantics<br />could be vacuously correct by accident, and thus the Capla programs would be too. This<br />work item is purely at the semantics level and does not touch the compiler. It is unclear<br />how difficult it is.<br /><br />If time permits or if some of the previous items end up being unreachable, a last objective<br />is to improve the interface with the Rocq proof assistant:<br /><br />5. Make it simpler to import Capla code inside Rocq to prove its correctness. Currently,<br />the process involves passing a debug option to the compiler and moving some Rocq files<br />around. Ideally, it should be possible to directly invoke the compiler from a Rocq session.<br />This work item does not involve the semantics and the formal proofs, but it might be<br />require touching the implementation of Rocq.</p>
Principales activités
<p>Software development in Rocq, development of<br />specifications and proofs, software experimentation, writing<br />documentation, contribution to the writing of scientific articles.</p>
Compétences
<p><br />Knowledge about the semantics of programming languages and their<br />implementation is required. Knowledge of the Rocq proof assistant or<br />of a closely-related formal system (e.g., Lean), is<br />required. Knowledge of French is not required.</p>
