Extension de ML avec raffinement (synthaxe, sémantiques et système de types)

Le raffinement est une méthode pour dériver des programmes corrects à partir de spécifications. Un langage de types expressif est un autre moyen d'assurer la correction des programmes. Nous proposons une extension du langage ML permettant de vérifier la correction des programmes ML en combinant ces deux approches : les programmes peuvent être construits par raffinements successifs de spécifications, la correction de chaque étape étant garantie par un système de types. Au niveau syntaxique, notre extension ajoute les types de base aux expressions, introduisant de ce fait du sous-déterminisme et des types dépendants. Elle intègre également une nouvelle construction, appelée application démoniaque, de manière à augmenter la puissance du langage de spécification. Nous étudions les sémantiques dénotationnelle et opérationnelle de l'extension proposée. Nous démontrons leur équivalence ainsi que leur conservativité par rapport à la sémantique habituelle de ML. Nous proposons également un système de génération d'obligations de preuve: si ces dernières sont prouvées correctes par l'utilisateur, alors la correction du programme vis-à-vis de sa spécification est garantie. Par ailleurs, un prototype de l'extension proposée a été implanté, fournissant de premiers résultats expérimentaux prometteurs. Enfin, l'ajout de caractéristiques propres à ML et manquantes dans notre extension est également discuté.Refinement is a method to derive correct programs from specifications. An expressive type language is another way to ensure program correctness. We propose an extension of ML mixing both above approaches: programs may be built by successive refinements of specifications and a type system ensures the correctness of each refinement step. At the syntactic level, our extension add base types into expressions, introducing undedeterminism and dependent types. It also introduces a new construct, called demonic application, which increases the expressiveness of the specification language. We study the denotational and operational semantics of this extension. We prove that their are equivalent and conservative with respect to the usual ML semantics. We also propose a system which generates proof obligations: their validities imply the correctness of the input program with respect to its specification is ensured. Besides, we have implemented a prototype and the first experimental results are promising. Additions of missing ML features are also discussed.ORSAY-PARIS 11-BU Sciences (914712101) / SudocSudocFranceF