Au cours des dernières années, les assistants de preuves on fait des progrès considérables et ont atteint un grand niveau de maturité. Ils ont permit la certification de programmes complexes tels que des compilateurs et même des systèmes d'exploitation. Néanmoins, l'utilisation d'un assistant de preuve requiert des compétences techniques très particulières, qui sont très éloignées de celles requises pour programmer de manière usuelle. Pour combler cet écart, nous entendons concevoir un langage de programmation de style ML supportant la preuve de programmes. Il combine au sein d'un même outil la flexibilité de ML et le fin niveau de spécification offert par un assistant de preuve. Autrement dit, le système peut être utilisé pour programmer de manière fonctionnelle et fortement typée tout en autorisant l'obtention de nouvelles 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é entre les programmes non typés, un type de fonction dépendant, la logique classique et du sous-typage. La combinaison de l'appel par valeurs,des fonctions dépendantes et de la logique classique est connu pour poser des problèmes de cohérence. Pour s'assurer de la correction du système (cohérence logique et sûreté à l'exécution), on propose un cadre théorique basé sur la réalisabilité classique de Krivine. La construction du modèle repose sur une propriété essentielle qui lie les différent niveaux d'interprétation des types d'une manière novatrice.On démontre aussi l'expressivité de notre système en se basant sur son implantation dans un prototype. Il peut être utilisé pour prouver des propriétés de programmes standards tels que la fonction « map »sur les listes ou le tri par insertion. / 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.

La thèse contribue à l’étude du λ-calcul non-typé de Church, un système de réécriture dont la règle principale est la β-réduction (formalisant l’exécution d’un programme). Nous nous concentrons sur la sémantique dénotationnelle, l’étude de modèles du λ-calcul interprétant de la même façon les λ-termes β-convertibles. On examine la sémantique relationnelle, une sémantique sensible aux ressources qui interprète les λ-termes comme des relations avec les entrées regroupées en multi-ensembles. Nous définissons une classe de modèles relationnels, les modèles de graphe relationnels (rgm’s), que nous étudions avec une approche issue de la théorie des types et de la démonstration, par le biais de certains systèmes de types avec intersection non-idémpotente. D’abord, nous découvrons la plus petite et la plus grande λ–théorie (théorie équationnelle étendant la β-conversion) représentées dans la classe. Ensuite, nous utilisons les rgm’s afin de résoudre le problème de l’adéquation complète pour la λ–théorie observationnelle de Morris, à savoir l’équivalence contextuelle de programmes que l’on obtient lorsqu’on prend les β-formes normales comme sorties observables. On résoudre le problème de différentes façons. En caractérisant la β-normalisabilité avec les types, nous découvrons une infinité de rgm’s complètement adéquats, que nous appelons uniformément sans fond. Puis, nous résolvons le problème de façon exhaustive, en prouvant qu’un rgm est complètement adéquat pour l’observabilité de Morris si et seulement si il est extensionnel (il modèle l’ŋ-conversion) et λ-König. Moralement un rgm est λ-König si tout arbre récursif infini a une branche infinie témoignée par un type non-bien-fondé / This thesis is a contribution to the study of Church’s untyped λ-calculus, a term rewritingsystem having the β-reduction (the formal counterpart of the idea of execution of programs) asmain rule. The focus is on denotational semantics, namely the investigation of mathematical models of the λ-calculus giving the same denotation to β-convertible λ-terms. We investigate relational semantics, a resource-sensitive semantics interpreting λ-terms as relations,with their inputs grouped together in multisets. We define a large class of relational models,called relational graph models (rgm’s), and we study them in a type/proof-theoretical way, using some non-idempotent intersection type systems. Firstly, we find the minimal and maximal λ-theories (equational theories extending -conversion) represented by the class.Then we use rgm’s to solve the full abstraction problem for Morris’s observational λ-theory,the contextual equivalence of programs that one gets by taking the β-normal forms asobservable outputs. We solve the problem in different ways. Through a type-theoretical characterization of β-normalizability, we find infinitely many fully abstract rgm’s, that wecall uniformly bottomless.We then give an exhaustive answer to the problem, by showing thatan rgm is fully abstract for Morris’s observability if and only if it is extensional (a model of ŋ-conversion) and λ-König. Intuitively an rgm is λ-König when every infinite computable tree has an infinite branch witnessed by some type of the model, where the witnessing is a property of non-well-foundedness on the type.