Sémantique et Implantation d'une Extension de ML pour la Preuve de Programmes

In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it remains very different from standard programming. To bridge this gap, we aim at designing an ML-style programming language with support for proofs of programs, combining in a single tool the flexibility of ML and the fine specification features of a proof assistant. In other words, the system should be suitable both for programming (in the strongly-typed, functional sense) and for gradually increasing the level of guarantees met by programs, on a by-need basis.We thus define and study a call-by-value language whose type system extends higher-order logic with an equality type over untyped programs, a dependent function type, classical logic and subtyping. The combination of call-by-value evaluation, dependent functions and classical logic is known to raise consistency issues. To ensure the correctness of the system (logical consistency and runtime safety), we design a theoretical framework based on Krivine's classical realisability. The construction of the model relies on an essential property linking the different levels of interpretation of types in a novel way.We finally demonstrate the expressive power of our system using our prototype implementation, by proving properties of standard programs like the map function on lists or the insertion sort.Au cours des dernières années, les assistants de preuves on fait des progrèsconsidérables et ont atteint un grand niveau de maturité. Ils ont permit lacertification de programmes complexes tels que des compilateurs et même dessystèmes d'exploitation. Néanmoins, l'utilisation d'un assistant de preuverequiert des compétences techniques très particulières, qui sont trèséloignées de celles requises pour programmer de manière usuelle. Pour comblercet écart, nous entendons concevoir un langage de programmation de style MLsupportant la preuve de programmes. Il combine au sein d'un même outil laflexibilité de ML et le fin niveau de spécification offert par un assistantde preuve. Autrement dit, le système peut être utilisé pour programmer demanière fonctionnelle et fortement typée tout en autorisant l'obtention denouvelles garanties au besoin.On étudie donc un langage en appel par valeurs dont le système de typeétend une logique d'ordre supérieur. Il comprend un type égalité entreles programmes non typés, un type de fonction dépendant, la logiqueclassique et du sous-typage. La combinaison de l'appel par valeurs,des fonctions dépendantes et de la logique classique est connu pourposer des problèmes de cohérence. Pour s'assurer de la correction dusystème (cohérence logique et sûreté à l'exécution), on propose uncadre théorique basé sur la réalisabilité classique de Krivine. Laconstruction du modèle repose sur une propriété essentielle qui lieles différent niveaux d'interprétation des types d'une manièrenovatrice.On démontre aussi l'expressivité de notre système en se basant surson implantation dans un prototype. Il peut être utilisé pour prouverdes propriétés de programmes standards tels que la fonction « map »sur les listes ou le tri par insertion