Les services informatiques, et particulièrement les services sur le Web, permettent le traitement ou l'échange d'informations. Leur composition ainsi que la construction de workflows à partir de services permettent la réalisation de tâches complexes. Toutefois, seules des informations utiles à leur gestion informatique (stockage, exécution, etc.) sont spécifiées dans les langages de description de services ou de compositions de services tels que WSDL, BPEL ou XPDL. Ces descriptions, essentiellement syntaxiques, ne sont pas suffisamment riches pour permettre une gestion complexe supportant la découverte, l'interopérabilité ou l'adaptativité de services au niveau sémantique. En effet, ces descriptions ne permettent pas de lier explicitement les services informatiques et les compositions qu'elles définissent aux fonctions et aux processus implémentés ainsi qu'aux concepts manipulés. Dans les domaines de l'ingénierie par exemple, l'activité de composition de services informatiques reste traditionnellement à la charge des ingénieurs. L'absence de sémantique explicite rend les services et workflows informatiques difficilement compréhensibles, réutilisables et composables pour les ingénieurs du domaine d'intérêt qui n'ont pas contribué à leur conception et ayant des connaissances techniques et informatiques en général limitées. Ces ingénieurs restent ainsi dépendants des développeurs de logiciels pour l'utilisation ou la composition de services informatiques. Pour apporter une solution aux problèmes évoqués, de récentes approches ont été proposées. Cependant, leurs mécanismes d'enrichissement sémantique ne séparent pas la partie syntaxique, utile au stockage ou à l'exécution, de la partie sémantique, utile à la découverte ou à la composition. En outre, ces mécanismes ne fournissent aucune classification hiérarchique ou relationnelle selon la sémantique des services informatiques. Pour remédier à ces limitations, nous proposons une approche basée sur la définition d'ontologies de services (conceptualisations partagées) et d'indexations sémantiques. Notre proposition s'appuie sur une architecture de persistance centrée autour des bases de données à base ontologique pour stocker et indexer les différents services ainsi que leurs compositions. La mise en oeuvre de notre approche consiste en un prototype logiciel implantant les concepts de service et de workflow sémantiques permettant de stocker, de rechercher, de remplacer, de réutiliser les services et les workflows informatiques existants et d'en construire de nouveaux de manière incrémentale. Ces travaux sont validés en étant appliqués au domaine de la modélisation géologique et de l'ingénierie pétrolière et plus particulièrement à l'interprétation sismique.

En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CIC car cela est ardu et fastidieux. Coq propose un environnement de programmation qui facilite la tâche en permettant d'écrire des programmes incrémentalement grâce à des constructions de haut niveau plus concises. Typiquement, les types dépendants imposent des contraintes fortes sur les données. Une analyse de cas peut n'avoir à traiter qu'un sous-ensemble des constructeurs d'un type algébrique, les autres étant impossibles par typage. Le type attendu dans chacun des cas varie en fonction du constructeur considéré. L'impossibilité de cas et les transformations de type doivent être explicitement écrites dans les termes de Coq. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation. Par ailleurs, il est nécessaire à l'interaction avec l'utilisateur de calculer des programmes du CIC sans faire exploser la taille syntaxique de la forme réduite. Cette thèse présente une machine abstraite conçu dans ce but. Enfin, les points fixes permettent une manipulation aisée des structure de données récursives. En contrepartie, il faut s'assurer que leur exécution termine systématiquement. Cette question sensible fait l'objet du dernier chapitre de cette thèse.