Plusieurs classes de solutions permettent d'exprimer des requêtes dans des langages de programmation: les interfaces spécifiques telles que JDBC, les mappings objet-relationnel ou object-relational mapping en anglais (ORMs) comme Hibernate, et les frameworks de requêtes intégrées au langage comme le framework LINQ de Microsoft. Cependant, la plupart de ces solutions ne permet de requêtes visant plusieurs bases de données en même temps, et aucune ne permet l'utilisation de logique d'application complexe dans des requêtes aux bases de données. Dans cette thèse, nous détaillons la création d'un framework de requêtes intégrées au langage nommé BOLDR qui permet d'évaluer dans les bases de données des requêtes écrites dans des langages de programmation généralistes qui contiennent de la logique d'application, et qui ciblent différentes bases de données potentiellement basées sur des modèles de données différents. Dans ce framework, les requêtes d'une application sont traduites vers une représentation intermédiaire de requêtes, puis réécrites pour éviter le phénomène "d'avalanche de requêtes" et pour profiter au maximum des capacités d'optimisation des bases de données, et enfin envoyées pour évaluation vers les bases de données ciblées et les résultats obtenus sont convertis dans le langage de programmation de l'application. Nos expériences montrent que les techniques implémentées dans ce framework sont applicables pour de véritables applications centrées données, et permettent de gérer efficacement un vaste champ de requêtes intégrées à des langages de programmation généralistes. / Several classes of solutions allow programming languages to express queries: Specific APIs such as JDBC, Object-Relational Mappings (ORMs) such as Hibernate, and language-integrated query frameworks such as Microsoft's LINQ. However, most of these solutions do not allow for efficient cross-databases queries, and none allow the use of complex application logic from the programming language in queries. In this thesis, we create a language-integrated query framework called BOLDR that, in particular, allows the evaluation in databases of queries written in general-purpose programming languages that contain application logic, and that target different databases of possibly different data models. In this framework, application queries are translated to an intermediate representation, then rewritten in order to avoid query avalanches and make the most out of database optimizations, and finally sent for evaluation to the corresponding databases and the results are converted back to the application. Our experiments show that the techniques we implemented are applicable to real-world database applications, successfully handling a variety of language-integrated queries with good performances.

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données. / This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications.