• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 94
  • 39
  • 9
  • Tagged with
  • 144
  • 75
  • 40
  • 40
  • 36
  • 34
  • 34
  • 32
  • 30
  • 22
  • 22
  • 22
  • 21
  • 21
  • 21
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
31

Langages fonctionnels, typage et interopérabilité : Objective Caml sur .NET

Montelatici, Raphaël 15 March 2007 (has links) (PDF)
La plate-forme .NET est un environnement d'exécution moderne et répandu, reposant sur une machine virtuelle qui interprète du code-octet typé. Elle prétend être parfaitement adaptée à l'exécution de composants écrits dans une grande variété de langages de programmation et faciliter leur interopération.<br /> En tant que langage fonctionnel statiquement typé avec polymorphisme paramétrique, Objective Caml présente des caractéristiques qui défient l'environnement d'exécution .NET et son système de types. Nous expérimentons ces difficultés dans un cadre pratique, par la conception et l'implantation de OCamIL, un compilateur complet pour Objective Caml qui produit du code-octet .NET vérifiable. Ses objectifs principaux sont la compatibilité et la possibilité d'interopérer.<br /> Ce travail met à l'épreuve les capacités de la plate-forme .NET autant que l'adéquation de l'implantation officielle de Objective Caml dans un tel projet (celle-ci est conçue pour un environnement d'exécution dénué de types ce qui explique qu'elle élimine les informations de types assez tôt dans la chaîne de compilation). Nous examinons la représentation des valeurs Caml et comparons deux stratégies : la reconstruction et la propagation de l'information de typage manquante. D'autres choix de conception décrits ici illustrent le compromis entre efficacité d'une part et lisibilité/interopérabilité de l'autre.<br /> Nous réalisons l'interopérabilité à l'aide d'un langage de description d'interface IDL qui construit un pont entre les deux systèmes de classes distincts utilisés par Objective Caml et l'environnement typé de .NET. Les bénéfices de l'interopération sont illustrés par des exemples non-triviaux.<br /> Au chapitre des performances, OCamIL occupe une place respectable au sein des compilateurs de langages fonctionnels sur .NET. Nous comparons également les exécutables .NET avec les programmes Objective Caml originaux.
32

INTEROPERABILITE DIRIGEE PAR LES MODELES :<br />Une Approche Orientée Produit pour l'interopérabilité des<br />systèmes d'entreprise.

Baïna, Salah 07 December 2006 (has links) (PDF)
Les travaux de la thèse présentent une approche pour l'interopérabilité entre les différents<br />modèles de produit, nous appellerons cette approche « l'interopérabilité orientée produit ».<br />Nous proposons ainsi un meta-modèle dont les instances jouent le rôle de passerelle de<br />communication entre différentes applications d'entreprise pour assurer l'interopérabilité des<br />parties de systèmes concernant le produit.<br />Nous nous sommes intéressés à formaliser un meta-modèle pour la définition du concept de<br />produit comme l'agrégation d'une partie physique représentant les éléments physiques du<br />produit et une partie informationnelle reprenant les éléments informationnels décrivant le<br />produit.<br />L'outillage et le prototypage du concept de produit holonique lors de la modélisation du<br />processus de fabrication dans l'entreprise ainsi que la prise en charge des mapping pour<br />l'interopérabilité s'appuient sur l'intégration du meta-modèle holonique dans un<br />environnement de modélisation d'entreprise particulier.<br />La phase de validation a été réalisée en deux parties représentées chacune par une application<br />industrielle. La première application se situe dans le cadre d'une collaboration avec le<br />département meunerie dans un grand groupe industriel, pour une application en<br />environnement réel de la modélisation holonique. L'objectif de cette application est de<br />concevoir un système de traçabilité pour les différents produits par les moulins du groupe.<br />Notre participation dans ce projet, a consisté en l'application de l'approche de modélisation<br />holonique pour la spécification, a priori, de l'ensemble des données et informations relatives<br />aux produits devant être prises en compte dans le système de traçabilité, et ainsi de générer de<br />manière automatique le schéma de données préliminaire du système. La seconde application<br />concerne la mise en œuvre de l'approche holonique pour une solution d'interopérabilité<br />orienté produit dans le cadre du pôle AIP Lorrain (AIPL).
33

Meta-modèles et modèles pour l'intégration et l'interopérabilité des applications d'entreprises de production

Panetto, Hervé 04 December 2006 (has links) (PDF)
L'intégration des systèmes consiste à assembler les différentes parties d'un système tout en assurant la compatibilité de l'assemblage ainsi que le bon fonctionnement du système complet. Depuis les années quatre-vingt-dix, l'intégration des systèmes d'entreprise a fait l'objet d'une attention croissante ; elle est ainsi devenue un thème de recherche développé dans plusieurs équipes universitaires et industrielles dans le monde autant que a suscité de nombreux travaux au sein des organisations scientifiques internationales, notamment IFAC et IFIP, et de normalisation, particulièrement IEC, ISO et CEN. Dans ce cadre, l'interopérabilité des systèmes est un moyen pour obtenir l'intégration, fondé sur un couplage faible des parties du système, basé sur la capacité des parties à communiquer entre elles pour accéder et faire appel à leurs fonctionnalités.<br />Plus récemment, au cours de la dernière décennie, une nouvelle approche d'ingénierie logicielle a été élaborée : l'ingénierie dirigée par les modèles. Dans cette nouvelle approche, les modèles occupent une place de premier plan parmi les artefacts d'ingénierie des systèmes. En effet, ils doivent être suffisamment précis afin de pouvoir être interprétés ou transformés par des outils logiciels, tout en étant mis en correspondance avec les démarches d'ingénierie système. Le rôle central des modèles dans le développement des capacités d'interopérabilité participe notablement à cette qualité, car les processus d'ingénierie de l'interopérabilité des applications sont basés sur des flux de modèles.<br /><br />Ce mémoire d'Habilitation à Diriger des Recherches est centré sur l'étude des modèles en vue de l'interopérabilité des systèmes, et plus particulièrement des systèmes d'entreprises, centrée sur la représentation des produits. Pour contribuer à la fiabilisation des modèles d'entreprise et de leur interrelations pour l'intégration forte des applications, le projet de recherche proposé dans ce mémoire a pour objectif, dans un contexte d'ingénierie système appliqué aux systèmes de systèmes, de définir, d'étendre et de formaliser les processus de modélisation des systèmes d'entreprise en tenant compte des connaissances, généralement non explicites, des acteurs de ces systèmes. Cette preuve de concept relatif à la formalisation de la connaissance des modèles se base sur la définition d'ontologies, ainsi que la mise en correspondance, la transformation et l'échange de modèles, permettant l'intégration des applications d'entreprise et assurant ainsi des flux d'informations cohérents entre tous les acteurs. Ils nécessitent ainsi de rendre explicite la connaissance tacite des modélisateurs (et opérateurs) sur les processus (et donc les modèles) dont ils sont responsables ou auteurs.
34

Contribution aux méthodes hybrides d'optimisation heuristique : Distribution et application à l'interopérabilité des systèmes d'information

El Hami, Norelislam 23 June 2012 (has links) (PDF)
Les travaux présentés dans ce mémoire proposent une nouvelle méthode d'optimisation globale dénommée MPSO-SA. Cette méthode hybride est le résultat d'un couplage d'une variante d'algorithme par Essaim de particules nommé MPSO (Particle Swarm Optimization) avec la méthode du recuit simulé nommé SA (Simulted Annealing). Les méthodes stochastiques ont connu une progression considérable pour la résolution de problèmes d'optimisation. Parmi ces méthodes, il y a la méthode Essaim de particules (PSO° qui est développée par [Eberhart et Kennedy (1995)]. Quant à la méthode recuit simulé (SA), elle provient du processus physique qui consiste à ordonner les atomes d'un cristal afin de former une structure cristalline parfaite. Pour illustrer les performances de la méthode MPSO-SA proposée, une comparaison avec MPSO et SA est effectuée sur des fonctions tests connues dans la littérature. La métode MPSO-SA est utilisée pour la résolution des problèmes réels interopérabilité des systèmes d'information, ainsi qu'aux problèmes d'optimisation et de fiabilité des structures mécaniques.
35

Interopérabilité Sémantique Multi-lingue des Ressources Lexicales en Données Liées Ouvertes / Semantic Interoperability of Multilingual Lexical Resources in Lexical Linked Data

Tchechmedjiev, Andon 14 October 2016 (has links)
Lorsqu’il s’agit la construction de ressources lexico-sémantiques multilingues, la première chose qui vient à l’esprit, et la nécessité que les ressources à alignées partagent le même format de données et la même représentations (interopérabilité représentationnelle). Avec l’apparition de standard tels que LMF et leur adaptation au web sémantique pour la production de ressources lexico- sémantiques multilingues en tant que données lexicales liées ouvertes (Ontolex), l’interopérabilité représentationnelle n’est plus un verrou majeur. Cependant, en ce qui concerne l’interopérabilité des alignements multilingues, le choix et la construction du pivot interlingue est l’un des obstacles principaux. Pour nombre de ressources (par ex. BabelNet, EuroWordNet), le choix est fait d’utiliser l’Anglais, ou une autre langue comme pivot interlingue. Ce choix mène à une perte de contraste dans les cas où des sens du Pivot ont des lexicalisations différentes dans la même acception dans plusieurs autres langues. L’utilisation d’une pivot à acceptions interlingues, solution proposée il y a déjà plus de 20 ans, pourrait être viable. Néanmoins, leur construction manuelle est trop ardue du fait du manque d’experts parlant assez de langues et leur construction automatique pose problème du fait de l’absence d’une formalisation et d’une caractérisation axiomatique permettant de garantir leur propriétés. Nous proposons dans cette thèse de d’abord formaliser l’architecture à pivot interlingue par acceptions, en développant une axiomatisation garantissant leurs propriétés. Nous proposons ensuite des algorithmes de construction initiale automatique en utilisant les propriétés combinatoires du graphe des alignements bilingues, mais aussi des algorithmes de mise à jour garantissant l’interopérabilité dynamique. Dans un deuxième temps, nous étudions de manière plus pratique sur DBNary, un extraction périodique de Wiktionary dans de nombreuses éditions de langues, afin de cerner les contraintes pratiques à l’application des algorithmes proposés. / When it comes to the construction of multilingual lexico-semantic resources, the first thing that comes to mind is that the resources we want to align, should share the same data model and format (representational interoperability). However, with the emergence of standards such as LMF and their implementation and widespread use for the production of resources as lexical linked data (Ontolex), representational interoperability has ceased to be a major challenge for the production of large-scale multilingual resources. However, as far as the interoperability of sense-level multi-lingual alignments is concerned, a major challenge is the choice of a suitable interlingual pivot. Many resources make the choice of using English senses as the pivot (e.g. BabelNet, EuroWordNet), although this choice leads to a loss of contrast between English senses that are lexicalized with a different words in other languages. The use of acception-based interlingual representations, a solution proposed over 20 years ago, could be viable. However, the manual construction of such language-independent pivot representations is very difficult due to the lack of expert speaking enough languages fluently and algorithms for their automatic constructions have never since materialized, mainly because of the lack of a formal axiomatic characterization that ensures the pre- servation of their correctness properties. In this thesis, we address this issue by first formalizing acception-based interlingual pivot architectures through a set of axiomatic constraints and rules that guarantee their correctness. Then, we propose algorithms for the initial construction and the update (dynamic interoperability) of interlingual acception-based multilingual resources by exploiting the combinatorial properties of pairwise bilingual translation graphs. Secondly, we study the practical considerations of applying our construction algorithms on a tangible resource, DBNary, a resource periodically extracted from Wiktionary in many languages in lexical linked data.
36

Contribution à une modélisation ontologique des informations tout au long du cycle de vie du produit / Towards an ontology-based infomation modelling along product lifecycle

Fortineau, Virginie 18 November 2013 (has links)
Les travaux de recherche de cette thèse portent sur la modélisation sémantique des informations industrielles, dans une approche og cycle de vie fg , de gestion des informations. Dans ce type d'approche, lever le verrou lié à l'interopérabilité des modèles d'information est une condition sine qua non à un échange d'information sans perte de flux sémantique. Jusqu'alors, des méthodes d'unification étaient envisagées, reposant sur l'utilisation mutuelle de modèles standards, tels que la norme STEP par exemple. Cependant, l'unification fait face à des limites en termes d'expressivité des modèles, de rigidité, et de perte de sémantique. Afin de lever ces limites, les paradigmes de modélisation évoluent et se tournent vers les ontologies d'inférence, outils du web sémantique.Dans cette thèse, nous proposons un cadre de modélisation sémantique général et une méthodologie de mise en place de ce cadre, qui reposent sur l'utilisation d'ontologies d'inférence. L'application du cadre de modélisation à un cas d'étude industriel, issu de l'ingénierie nucléaire (plus particulièrement l'expression et l'exécution des règles métier), permet alors d'évaluer les apports et limites des ontologies en tant que paradigme de modélisation. Les limites les plus importantes que nous identifions sur l'Open World Assumption, le manque de langage de règles performant et le manque d'outils d'implémentation robustes pour des applications à large échelle. Le développement d'un démonstrateur pour le cas d'étude industriel permet finalement de tendre vers une solution mixte, où les ontologies sont utilisées localement, afin d'en exploiter les divers avantages de manière optimale. / The present research study deals with industrial information modelling in a lifecycle management approach. In this context, achieving semantic interoperability is an important issue to guaranty the quality of information storage, exchange and reuse. Current solutions are based on unification approaches and use standard models as shared information representation. However, unification approches suffer from a lack of expressivity and flexibility. To overcome this issue, ontologies are proposed as a new modelling paradigm in order to perform federativ interoperability.This research focuses on inference ontologies and investigates the use of those semantic web-based technologies for a large scale industrial application. An ontology-based framework and a modelling methodology are therefore proposed and evaluated on a industrial use case in the nuclear industry. The application raises modelling issues like the Open World Assumption, the lack of a real integrated rule approach, and the robustness of implementation tools. The industrial use case is implemented within a demonstrator, that finally allows to propose an hybrid solution, where ontologies are locally used.end{abstract}
37

Systèmes mobiles émergents dans l’IoT : de l’interopérabilité au niveau middleware de communication à l’analyse de la qualité de service associée / Enabling emergent mobile systems in the IoT : from middleware-layer communication interoperability to associated QoS analysis

Bouloukakis, Georgios 01 August 2017 (has links)
Les applications de l'Internet des objets (IdO/IoT) se composent de divers objets en grande partie mobiles et avec des ressources limitées ou riches. Des tels dispositifs exigent des interactions légères et faiblement couplées en termes de temps, d'espace et de synchronisation. Les protocoles au niveau middleware de l'IoT prennent en charge un ou plusieurs types d'interaction assurant la communication entre objets. De plus, ils supportent différents niveaux de Qualité de service (QDS) pour cette communication par rapport aux ressources disponibles sur les dispositifs et les réseaux. Les dispositifs utilisant le même protocole middleware interagissent de manière homogène, car ils exploitent les mêmes caractéristiques fonctionnelles et de QDS. Cependant, la profusion de protocoles middleware pour l'IoT se traduit par des objets très hétérogènes. Cela nécessite des solutions d'interopérabilité avancées intégrées à des techniques de modélisation et d'évaluation de la QDS. La principale contribution de cette thèse est d'introduire une approche et de fournir une plate-forme pour la synthèse automatique des artefacts logiciels permettant l'interopérabilité. De tels artefacts permettent l'interconnexion entre des objets mobiles qui utilisent des protocoles hétérogènes au niveau middleware. Notre plate-forme prend en charge l'évaluation de l'effectivité de l'interconnexion en termes de la QDS de bout en bout. Plus précisément, nous dérivons des conditions formelles pour des interactions réussies, et nous permettons la modélisation et l'analyse des performances ainsi que le réglage du système de bout en bout, tout en considérant plusieurs paramètres système pour l'IoT mobile. / Internet of Things (IoT) applications consist of diverse Things including both resource-constrained/rich devices with a considerable portion being mobile. Such devices demand lightweight, loosely coupled interactions in terms of time, space, and synchronization. IoT middleware protocols support one or more interaction types (e.g., asynchronous messaging, streaming) ensuring Thing communication. Additionally, they introduce different Quality of Service (QoS) features for this communication with respect to available device and network resources. Things employing the same middleware protocol interact homogeneously, since they exploit the same functional and QoS features. However, the profusion of developed IoT middleware protocols introduces technology diversity which results in highly heterogeneous Things. Interconnecting heterogeneous Things requires mapping both their functional and QoS features. This calls for advanced interoperability solutions integrated with QoS modeling and evaluation techniques. The main contribution of this thesis is to introduce an approach and provide a supporting platform for the automated synthesis of interoperability software artifacts. Such artifacts enable the interconnection between mobile Things that employ heterogeneous middleware protocols. Our platform further supports evaluating the effectiveness of the interconnection in terms of end-to-end QoS. More specifically, we derive formal conditions for successful interactions, and we enable performance modeling and analysis as well as end-to-end system tuning, while considering several system parameters related to the mobile IoT.
38

Représentations et dynamique de la ville virtuelle / Representations and dynamics of the virtual city

Pedrinis, Frédéric 17 October 2017 (has links)
Les modélisations 3D de ville se multiplient à travers le monde et deviennent aujourd’hui accessibles grâce à la volonté des communes de les proposer librement. Il est ainsi aujourd’hui possible d’accéder à plusieurs milliers de kilomètres carrés de territoires urbains modélisés en 3D. Nous présentons dans cette thèse un ensemble de méthodes permettant d’enrichir un modèle virtuel 3D de ville, de l’organiser afin de faciliter son utilisation, puis de l’analyser en détectant les changements entre deux millésimes ou en mesurant son ambiance visuelle selon les besoins de l’utilisateur. Nous proposons dans un premier temps un algorithme permettant de compléter un modèle 3D en y adjoignant une définition sémantique grâce au cadastre, ainsi qu’une méthode de calcul de la canopée végétale 3D par croisement de données. Puis nous proposons des stratégies d’organisation du modèle 3D de la ville selon des critères géométriques et sémantiques afin de faciliter son parcours. Nous présentons ensuite des méthodes comparant deux millésimes de données représentant un même territoire dans le but de produire un unique modèle temporel contenant un ensemble de versions. Enfin, nous cherchons à mesurer l’ambiance visuelle de la ville via l’analyse de la composition d’un champ de vision ainsi que de l’ensoleillement et des ombres portées présentes sur un territoire. Ces mesures peuvent être liées à des données externes afin de proposer de multiples interprétations en fonction des besoins de l’utilisateur.Tous ces travaux se font dans un contexte d’interopérabilité et de généricité puisqu’ils ont pour objectif de pouvoir être utilisés avec des jeux de données provenant du monde entier. Nous basons donc nos méthodes sur l’utilisation de standards internationaux aussi bien pour les données en entrée que pour les résultats en sortie. Il est ainsi possible, dans le cadre d’une approche voulue dans un contexte de pluralité scientifique au sein du LabEx IMU, de mettre à disposition de la communauté les résultats mais aussi nos algorithmes proposés au sein d’un logiciel développé en open source. / 3D virtual models of cities are multiplying throughout the world and now become accessible thanks to the will of the communes to propose them freely. Today, it is possible to access several thousand square kilometres of urban territories modelled in 3D.We present in this thesis a set of methods to enrich a 3D virtual city model, organize it to facilitate its use and then analyse it by detecting changes between two vintages or by measuring its visual atmosphere according to the user’s needs. We first propose an algorithm to complete a 3D model by adding a semantic definition thanks to the cadastre, and a method to compute the 3D plant canopy by crossing data. Then we propose strategies to organize the 3D model of the city according to geometric and semantic criteria in order to facilitate its browsing. We then present methods comparing two vintages of data representing the same territory in order to produce a single temporal model containing a set of versions. Finally, we try to measure the visual atmosphere of the city by analysing the composition of a field of vision as well as the amount of sunshine and the shadows on a territory. These measurements can be linked to external data in order to propose multiple interpretations according to the user’s needs.All this work is done in a context of interoperability and genericity since it aims to be used with datasets from all over the world. We therefore base our methods on the use of international standards for both input and output data. It is thus possible, in a context of scientific plurality within the LabEx IMU, to make available to the community the results but also our algorithms proposed within an open source developed software.
39

Adaptation dynamique de données pour la synthèse et le déploiement de protocoles de médiation / Dynamic Data Adaptation for the Synthesis and Deployment of Protocol Mediators

Andriescu, Emil-Mircea 08 February 2016 (has links)
Dans la plupart des systèmes disponibles aujourd'hui l'interopérabilité est fournie comme une capacité statique qui est le résultat d'une intégration conçue manuellement. En conséquence, un nombre important de systèmes fonctionnellement compatibles ne sont pas conçues pour être interopérables. L'objectif de cette thèse est de permettre l'interopérabilité automatisée des protocoles pour les systèmes, services et applications à travers des médiateurs de protocoles synthétisés dynamiquement. Les médiateurs représentent des composants logiciels qui peuvent coordonner les interactions entre deux ou plusieurs systèmes fonctionnellement compatibles, en utilisant les différents moyens de communication (réseaux IP, IPC, la mémoire partagée, etc.). Les médiateurs synthétisés dynamiquement devraient permettre aux applications de s'adapter sans difficulté aux protocoles a priori inconnus, soutiennent l'évolution de ces protocoles tout en contournant les contraintes des systèmes du monde réel, comme celles introduites par la mobilité de l'appareil et des systèmes d'exploitation. Dans cette thèse, nous nous concentrons sur les problèmes de recherche liés à l'automatisation du processus d'adaptation de données dans le cadre de la médiation de protocoles. L'adaptation des données est une étape clé dans la médiation de protocoles qui ne peut pas être résolu indépendamment. Cette dépendance devient visible lorsque les systèmes reposant sur des piles de protocoles complexes doivent être rendus interopérables, malgré les dépendances inter-couche à l'intérieur des données échangées. Il y a la nécessité d'un cadre qui synthétise les médiateurs, tout en tenant compte de l’adaptation de données. / In most systems available today interoperability is provided as a static capability that is the result of manually designed and hand coded integration. In consequence, a substantial number of functionally-compatible systems are not conceived to be interoperable. The focus of this thesis is to enable automated protocol interoperability for systems, services and applications through the means of dynamically synthesized protocol mediators. Protocol mediators represent concrete software components which can coordinate interactions between two or more functionally-compatible systems, relying on various means of communication (IP networks, personal area networks, inter-process communication, shared memory, etc.). Dynamically synthesised mediators should allow applications to seamlessly adapt to a priori unknown protocols, support the evolution of such protocols while circumventing real-world system constraints, such as those introduced by device mobility and operating system differences. In this thesis we focus on the research problems related to automating the process of data adaptation in the context of protocol mediation. Data adaptation is a key phase in protocol mediation that cannot be solved independently. This strong dependence becomes visible when systems relying on multilayer protocol stacks have to be made interoperable, despite cross-layer dependencies inside the exchanged data. There is the need of a frame- work that synthesises mediators while taking into account cross-layer data adaptation.
40

Object-Oriented Mechanisms for Interoperability Between Proof Systems / Mécanismes orientés objet pour l’interopérabilité entre systèmes de preuve

Cauderlier, Raphaël 10 October 2016 (has links)
Dedukti est un cadre logique résultant de la combinaison du typage dépendant et de la réécriture. Il permet d'encoder de nombreux systèmes logiques au moyen de plongements superficiels qui préservent la notion de réduction. Ces traductions de systèmes logiques dans un format commun sont une première étape nécessaire à l'échange de preuves entre ces systèmes. Cet objectif d'interopérabilité des systèmes de preuve est la motivation principale de cette thèse. Pour y parvenir, nous nous inspirons du monde des langages de programmation et plus particulièrement des langages orientés-objet parce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation, de modularité et de définitions par défaut. Pour cette raison, nous commençons par une traduction superficielle d'un calcul orienté-objet en Dedukti. L'aspect le plus intéressant de cette traduction est le traitement du sous-typage. Malheureusement, ce calcul orienté-objet ne semble pas adapté à l'incorporation de traits logiques. Afin de continuer, nous devons restreindre les mécanismes orientés-objet à des mécanismes statiques, plus faciles à combiner avec la logique et apparemment suffisant pour notre objectif d'interopérabilité. Une telle combinaison de mécanismes orientés-objet et de logique est présente dans l'environnement FoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dans Dedukti. Les difficultés principales proviennent de l'intégration de Zenon, le prouveur automatique de théorèmes sur lequel FoCaLiZe repose, et de la traduction du langage d'implantation fonctionnel de FoCaLiZe qui présente deux constructions qui n'ont pas de correspondance simple en Dedukti : le filtrage de motif local et la récursivité. Nous démontrons finalement comment notre encodage de FoCaLiZe dans Dedukti peut servir en pratique à l'interopérabilité entre des systèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviter de trop renforcer la théorie dans laquelle la preuve finale est obtenue, nous proposons d'utiliser Dedukti en tant que méta-langage pour éliminer des axiomes superflus. / Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis.To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms.

Page generated in 0.0851 seconds