Séminaire Cambium, Inria Paris
                                 Amphi Lions
                           Vendredi 13 juin, 10h30

                                 Josué Moreau
                             Inria Saclay et LMF

                A safe low-level language for computer algebra
                      and its formally verified compiler

I will present Capla, a programming language for writing low-level libraries
for computer algebra systems. Such libraries (GMP, BLAS/LAPACK, etc) are
usually written in C, Fortran, and Assembly, and make heavy use of arrays and
pointers. The proposed language is halfway between C and Rust with a type
system similar to the one of SPARK. It does not have any undefined behavior
and is designed to ease the deductive verification of programs, while being
low-level enough to be suitable for this kind of computationally intensive
applications. I have also implemented a compiler for this language, based on
the CompCert compiler. The safety of the language has been formally proved
using the Rocq proof assistant, and so has the property of semantics
preservation for the compiler.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.