Search

The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches., Comment: In Proceedings F-IDE 2019, arXiv:1912.09611

This thesis describes the construction of an environment to develop certified computer algebra libraries. First, we present species, the structures used to describe specifications, by multiple inheritance, refinement and parameterization. Collections are built by encapsulation of species and form the user library. We also define the static analyses that guarantee the correction of a species definition. Then, we study the compilation of species and collections into the programming language OCAML, with the use of OCAML's objects and modules. After that, we detail the translation into the proof language COQ, the late binding being translated by lambda-abstractions. We then show how this technique can be used to optimise OCAML executables. Last, we prove that the analyses performed by the compiler, as well as the translation mechanisms are correct with respect to the species formalisation made previously in COQ., Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.