This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Les systèmes informatiques envahissent de plus en plus notre quotidien, en allant de la plus simple application de lecture des fichiers audio, à la plus critique comme les voitures et les avions. Dans les systèmes critiques, la validation par vérification formelle s'impose. Cette thèse s'inscrit dans ce cadre et tend à doter le langage UML, langage de modélisation standard de facto, d'une sémantique formelle pour des finalités de vérification. En premier lieu, nous avons analysé et révisé le fondement théorique des principales approches de formalisation et de vérification issues de la littérature et se focalisant sur le langage UML, ses profils et les concepts des réseaux de Petri (RdPs). En deuxième lieu, nous avons proposé une nouvelle approche hiérarchique de formalisation des diagrammes globaux d'interactions (IOD). En se basant sur ce point, nous avons développé des formalismes temporels et temporisés des diagrammes de Timing UML2 (TD), appliqués par des exemples d'illustration. Ensuite, nous avons conçu une approche de vérification sur les approches développées, s'intéressant aux Systèmes Temps Réel (STRs), utilisant l'extension temporelle du langage des contraintes objets OCL/Temps Réel (OCL TR), le profil UML MARTE et la logique temporelle temporisée (TCTL), exploitée d'une technique de vérification automatique après la transformation du modèle (Model Checking). Enfin, nous avons appliqué les formalismes proposés sur une étude de cas, afin de garantir leurs efficacités logique et temporelle. / The computer systems have increasingly invaded our daily lives from the simplest application as audio files reading to the most critical one as cars and airplanes. For critical systems, the validation by the formal verification is required. This Thesis concerns this area of research and aims to ensure the betterment of UML language, which is the de facto standard, with formal semantics for verification finality. For the first part, we have analyzed and revised the theoretical foundations the existing formal verification methods used UML, their profiles and the basic concepts of the Petri nets (PNs). For the second part, we have created a novel hierarchical approach to formalize the Interaction Overview Diagrams (IOD). Based on this idea, we have developed temporal formalisms based on the UML2 Timing Diagrams (TD), applied by illustration examples. Then, we have proposed a Formal Verification approach based on last formalisms which are interested in Real Time Systems (RTS) and employ the temporal extension of the Object Constraints language (OCL/Real Time) (OCL TR), the UML MARTE profile and the timed computation Tree logic (TCTL), given by the Model Checking technique after the model's transformation. Finally, we have applied all the proposed formalisms through a case study, in order to ensure its logical and temporal efficiency.

La problématique de cette thèse est celle de la formalisation du travail domestique. Au-delà de la mise en œuvre de la politique des titres-services, cette thèse ouvre le questionnement sur les possibilités et le limites de la professionnalisation d’une quelconque politique pour le travail domestique. Sur base de notre recherche qualitative, trois constats inédits émanent de nos résultats.Le premier constat inédit émerge de l’étude de la politique des titres-services et de sa mise en œuvre en Région bruxelloise. Celle-ci a montré que les entreprises agréées en titres-services ne veulent pas embaucher des chercheures d’emploi de longue durée, qu’elles associent aux "Belges" et au manque de motivation à travailler dans le secteur. Les entreprises cherchent principalement à engager des travailleuses migrantes avec expérience sur le marché au noir et qui, de préférence, amènent leur clientèle avec elles. Ces travailleuses sont plus autonomes et exigent très peu de travail de la part des entreprises de titres-services. Cette préférence de recrutement des entreprises agréées va jusqu’à mettre en place des pratiques d’évitement des circuits officiels d’offre d’emploi. Ce constat fait ressortir en outre l’importance des liens ethniques dans la formation du marché du travail domestique formel. Le deuxième constat inédit est le rôle de la régularité de séjour comme déterminant pour l’accès à une vraie transformation identitaire et l’émancipation des travailleuses domestiques migrantes, en opposition à l’accès à un travail formel. Être "migrante sans papiers" et les conséquences de ce (manque de) statut dans les sociétés d’accueil ont déjà été décrites par plusieurs auteurs (Andall 2000; Anderson 2000; Parreñas 2001; Lutz 2011; Ambrosini 2012; Schwenken & Heimeshoff 2013). Nos analyses démontrent, par la situation contraire du passage à la régularité de séjour et à la formalité du travail, que l’entrée dans le travail formel est incapable d’amener seule une vraie transformation identitaire. Ainsi, si du point de vue statutaire les travailleuses en titres-services ont expérimenté un type de reconnaissance par la fiche de paie, les droits sociaux et un salaire direct et indirect, leur vie dans les faits n’a pas été changée et elles continuent à travailler aux mêmes endroits dans des conditions similaires. Et surtout, elles continuent à être vues de la même manière par elles-mêmes, par leurs employeuses devenues clientes et par la société. Enfin, l’opportunité d’un marché du travail formel est insuffisante pour résoudre la question de l’empowerment des travailleuses migrantes et de l’accomplissement de la professionnalisation – un processus en cours mais qui n’avance que lentement.Le troisième constat inédit de cette thèse est l’évidence que le règlement des titres-services et la logique qui structure cette politique ne favorisent ni la qualité d’emploi ni la valorisation de la profession, pour plusieurs raisons, entre autres la libre concurrence de ce quasi-marché, le fait que les travailleuses sont des salariées "entrepreneures d’elles-mêmes" et le manque de responsabilisation des clientes. / This PhD investigates the transition of the domestic work market in Brussels to formalization through the implementation of the housework voucher policy by the Belgian government in 2004 (the “titres-services” policy).Now existing for about ten years, one can say that the voucher policy has been a success in bringing from the shadow to formal market many domestic work employers and workers. In terms of valorization of paid domestic work, however, changes were meagre: if the housework voucher opens to domestic workers the possibility to access a formal job and its related social rights, domestic work in Brussels is still not attractive enough for nationals and is dominated by mainly newly arrived migrant women. The fact the work is formal does not change the image of the job as a ‘dirty work’. The main beneficiaries of the policy are, in fine, middle or upper classes, which can achieve work/life balance by meeting their demand of housework services at a much lower price than they used to pay in the informal sector.This PhD brings up three new results.Firstly, authorized voucher service companies avoid hiring job-seekers, although job creation is one of the policy goals. Companies prefer to hire workers that were previously in the informal domestic work market, as they consider these workers are used to the job, motivated and often bring their clients with them.Secondly, the migrant status of domestic workers switching to the formal market appears as a decisive factor for them to experience a change in their identity as workers and citizens. The mere change from an informal labor market to a formal labor market is insufficient for the workers to challenge their (often low) self-esteem and to allow them empower themselves (Adjamago & Calvès 2012). Thirdly, this research brings evidence that the voucher service system fails to enhance job quality and to upgrade the domestic work sector. Among other factors, because of the livre market competition, voucher employees being “entrepreneurs without enterprise” (Granovetter 1995), and the lack of voucher clients’ responsibility within the policy. This PhD research shows that the commodification of domestic work in Brussels did not change the fact that domestic tasks are gendered as ‘women’s work’ and hence did not bring changes whereby couples share the tasks. Besides, voucher agency publicities and leaflets reflect this gendered norm, in focusing on woman’s choice to commodify domestic tasks and earn ‘quality time’ with her beloved ones or for herself.Finally, it points policymaking difficulties in bringing a specific job, historically informal and personalized, to the formal labor market. Policymaking cannot evade the question of who is doing the housework, and should therefore look at the interaction of care, gender and migration regimes. Otherwise, gender equality in the labor market will continue to be met only by middle and upper class, and only through domestic work outsourcing (to other women), perpetuating gender, class and 'race' dominating positions. / Doctorat en Sciences politiques et sociales / info:eu-repo/semantics/nonPublished

La recherche d'information juridique en droit allemand et en droit français dans le domaine " informatique et droit " oblige à définir le droit dont on recherche l'existence dans chaque culture. La théorie pure du droit, telle qu'interprétée par Norberto Bobbio, propose les éléments d'une telle définition en excluant toute considération axiologique. Une norme juridique est une obligation, une interdiction, une permission ou une définition. Chaque norme a quatre domaines de validité, déterminés ou indéterminés : temporel, géographique, personnel et matériel. L'action prescrite et le contenu de la définition ne peuvent être formalisés qu'au moyen des concepts employés. Chaque signifiant employé dans une norme correspond à un signifié qui n'existe que dans les domaines de validité de la norme qui l'emploie. Une grammaire générative et un thésaurus de concepts permettent de formaliser les normes juridiques et d'en faire un traitement automatique. En particulier la recherche d'information juridique peut être faite grâce aux éléments de la norme juridique. La recherche d'information juridique est un apprentissage qui peut être réalisé à l'aide d'une encyclopédie juridique organisée au moyen d'hyperliens.

By extending Husserl’s own historico-critical study to include the conceptual mathematics of more contemporary times – specifically category theory and its emphatic development since the second half of the 20th century – this paper claims that the delineation between mathematics and philosophy must be completely revisited. It will be contended that Husserl’s phenomenological work was very much influenced by the discoveries and limitations of the formal mathematics being developed at Göttingen during his tenure there and that, subsequently, the rôle he envisaged for his material a priori science is heavily dependent upon his conception of the definite manifold. Motivating these contentions is the idea of a mathematics which would go beyond the constraints of formal ontology and subsequently achieve coherence with the full sense of transcendental phenomenology. While this final point will be by no means proven within the confines of this paper it is hoped that the very fact of opening up for the possibility of such an idea will act as a supporting argument to the overriding thesis that the relationship between mathematics and phenomenology must be problematised.

Notre recherche étudie les modifications dans la structure de l’entreprise occasionnées par la mise en œuvre de l’innovation ouverte. Plus précisément, nous nous intéressons aux modifications qui ont lieu dans la structure organisationnelle profonde et formelle de l’entreprise. Nous étudions ces modifications en mobilisant des données primaires (entretiens semi-directifs) et secondaires (rapports annuels et articles de presse) issues de neuf entreprises. Les résultats consistent en une nouvelle définition de l’innovation ouverte entrante, en un modèle contingent de l’innovation ouverte au niveau de l’entreprise et en une compréhension approfondie des modifications observées dans la structure organisationnelle profonde et formelle. La définition de l’innovation ouverte que nous proposons insiste sur trois aspects importants : l’intégration de l’ouverture dans la stratégie de l’entreprise en matière d’innovation, le caractère fréquent des collaborations et le caractère systématique de celles-ci. / This thesis studies the changes in the organizational structure determined by the implementation of open innovation. Specifically, we consider the changes in the deep and formal structure of a firm. We study these changes in nine firms by using primary data collected through semi-structured interviews and secondary data consisting of firms’ annual reports and journal articles. Our results consist of a new definition of inbound open innovation, a proposition of a contingency model of open innovation at firm level and a deep understanding of the way open innovation impacts the firm. The definition of inbound open innovation we propose emphasizes three main aspects : the integration the openness of innovation into the firm’s formal innovation strategy and the systematic and frequent use of collaborations with various actors in the innovation process.

Cette thèse porte sur la transformation automatique et sémantique de règles métiers en des règles formelles. Ces règles métiers sont originellement rédigées sous la forme de textes en langage naturel, de tableaux et d'images. L'objectif est de mettre à la disposition des experts métiers, un ensemble de services leur permettant d'élaborer des corpus de règles métiers formelles. Le domaine de la Construction est le champ d'application de ces travaux. Disposer d'une version formelle et exécutable de ces règles métiers servira à effectuer des contrôles de conformité automatique sur les maquettes numériques des projets de construction en cours de conception.Pour cela, nous avons mis à disposition des experts métiers les deux principales contributions de cette thèse. La première est la mise sur pied d'un langage naturel contrôlé, dénommé RAINS. Il permet aux experts métiers de réécrire les règles métiers sous la forme de règles formelles. Les règles RAINS se composent de termes du vocabulaire métier et de mots réservés tels que les fonctions de comparaisons, les marques de négation et de quantification universelle et les littéraux. Chaque règle RAINS a une sémantique formelle unique qui s'appuie sur les standards du web sémantique. La seconde contribution majeure est un service de formalisation des règles métiers. Ce service implémente une approche de formalisation proposée dans le cadre de cette thèse et dénommée FORSA. Ce service propose des versions RAINS des règles métiers en langage naturel qui lui sont soumises. FORSA fait appel à des outils du traitement automatique du langage naturel et à des heuristiques. Pour évaluer FORSA, nous avons mis sur pied un benchmark adapté à la tâche de formalisation des règles métiers. Les données de ce benchmark sont issues de normes du domaine de la Construction / This thesis focuses on automatic and semantic transformation of business rules into formal rules. These business rules are originally drafted in the form of natural language text, tables and images. Our goal is to provide to business experts a set of services allowing them to develop corpora of formal business rules. We carry out this work in the field of building engineering construction. Having formal and executable versions of the business rules enables to perform automatic compliance checking of digital mock-ups of construction projects under design.For this we made available to business experts, the two main contributions of this thesis. The first is the development of a controlled natural language, called RAINS. It allows business experts to rewrite business rules in the form of formal rules. A RAINS rule consists of terms of the business vocabulary and reserved words such as comparison predicates, negation and universal quantification markers and literals. Each RAINS rule has a unique formal semantics which is based on the standards of the Semantic Web. The second major contribution is a service for formalization of business rules. This service implements a formalized approach proposed in this thesis and called FORSA. This service offers RAINS versions of natural language business rules submitted to it. FORSA uses natural language processing tools and heuristics. To evaluate FORSA, we have set up a benchmark adapted to the formalization of business rules task. The dataset from this benchmark are from norms in the field of Construction

Ce travail de thèse a été initié par Renault, en collaboration avec le Centre de Recherche en Automatique de Nancy (CRAN), dans le but de poser les bases d'une méthodologie générique permettant d'évaluer l'état de santé de moyens de production. Cette méthodologie est issue d’une réflexion conjointe machine - produit en lien avec les exigences industrielles. La méthodologie proposée est basée sur une approche PHM (Prognostics and Health Management) et est structurée en cinq étapes séquentielles. Les deux premières étapes sont développées dans ce travail de thèse et en constituent les contributions scientifiques majeures. La première originalité représente la formalisation des connaissance issues de la relation machine-produit. Cette connaissance est basée sur l'extension de méthodes existantes telle que l’AMDEC et l’HAZOP. La formalisation des concepts de connaissance et de leurs interactions est matérialisée au moyen d'une méta-modélisation basée sur une modélisation UML (Unified Modelling Language). Cette contribution conduit à l'identification de paramètres pertinents à surveiller, depuis le niveau du composant jusqu'au niveau de la machine. Ces paramètres servent ensuite d’entrée au processus d'élaboration du bilan de santé machine, qui représente la deuxième originalité de la thèse. L'élaboration de ces indicateurs de santé est basée sur des méthodes d’agrégation, telle que l'intégrale de Choquet, soulevant la problématique de l'identification des capacités. De cette façon, il est proposé un modèle global d'optimisation de l'identification des capacités multi-niveaux du système à travers l’utilisation d’Algorithmes Génétiques. La faisabilité et l'intérêt d'une telle démarche sont démontrés sur le cas de la machine-outil située à l'usine RENAULT de Cléon / This PhD work has been initiated by Renault, in collaboration with Nancy Research Centre in Automatic Control (CRAN), with the aim to propose the foundation of a generic PHM-based methodology leading to machine health check regarding machine-product joint consideration and facing industrial requirements. The proposed PHM-based methodology is structured in five steps. The two first steps are developed in this PhD work and constitute the major contributions. The first originality represents the formalization of machine-product relationship knowledge based on the extension of well-known functioning/dysfunctioning analysis methods. The formalization is materialized by means of meta-modelling based on UML (Unified Modelling Language). This contribution leads to the identification of relevant parameters to be monitored, from component up to machine level. These parameters serve as a basis of the machine health check elaboration. The second major originality of the thesis aims at the definition of health check elaboration principles from the previously identified monitoring parameters and formalized system knowledge. Elaboration of such health indicators is based on Choquet integral as aggregation method, raising the issue of capacity identification. In this way, it is proposed a global optimization model of capacity identification according to system multi-level, by the use of Genetic Algorithms. Both contributions are developed with the objective to be generic (not only oriented on a specific class of equipment), according to industrial needs. The feasibility and the interests of such approach are shown on the case of machine tool located in RENAULT Cléon Factory

La réutilisation d'applications n'est pas un problème récent et de nombreux travaux ont étudié différentes façons de réutiliser tout ou partie d'une application. L'apparition des services et des composants au niveau fonctionnel facilite la construction et l'extension d'applications par composition de fonctionnalités indépendantes. En parallèle, des travaux sur les Interfaces Homme-Machine (IHM) proposent des solutions pour créer des IHM par composition d'IHM existantes. Mais ce n'est que récemment que des travaux se sont intéressés à composer l'ensemble d'une application. Malgré cela, ils ne proposent que des compositions simples tant au niveau des IHM que fonctionnel. Ces travaux de thèse proposent une approche pour faciliter le travail du développeur en lui permettant de réutiliser l'intégralité des applications à composer, c'est-à-dire, la partie fonctionnelle, l'IHM et les interactions entre l'IHM et la partie fonctionnelle. La proposition faite dans cette thèse lui permet de continuer d'utiliser les outils industriels dont il dispose pour composer les parties fonctionnelles des applications. Ainsi, c'est au travers de cette composition fonctionnelle ainsi que des interactions entre la partie fonctionnelle et l'IHM présentes dans les applications que se fera l'identification des éléments d'IHM à conserver et la création de l'application résultante. Cette approche repose sur un méta-modèle AliasComponent qui fournit une architecture à base de composants permettant de décrire à la fois les applications (en distinguant la partie fonctionnelle, les IHM et les interactions entre les deux) et la composition fonctionnelle. Ce méta-modèle permet ainsi d'extraire des applications existantes et de la composition fonctionnelle l'ensemble des informations essentielles à la réalisation de la composition des applications. Elle s'appuie aussi sur une formalisation qui permet la réalisation de la composition, c'est-à-dire, la déduction des éléments d'IHM à conserver, la détection de doublons non identiques (lorsque plusieurs widgets différents peuvent convenir), l'aide à la résolution de ceux-ci et la création de l'application résultante de la composition. Cette formalisation pose également les propriétés que doivent respecter les applications et le résultat de la composition assurant ainsi une application résultante fonctionnelle. Le méta-modèle et la formalisation sont intégrés au sein d'un processus d'aide à la composition. La solution proposée a, quant à elle, été mise en oeuvre au sein d'un atelier d'aide à la composition qui a permis de valider l'approche.

Nous proposons de traiter dans cette thèse, une partie du vaste domaine de la recherche dans le domaine des incendies de forêt. Nous nous intéressons plus particulièrement à la formalisation des connaissances (structuration des connaissances et de leurs interrelations) pour l'analyse du comportement des feux de forêt et plus précisément pour la modélisation de la vitesse de propagation d'un front de flammes. Le système incendie de forêt, de par sa complexité, doit être appréhendé par une démarche modélisatrice du phénomène (expérimentation, modélisation et validation). Nous proposons dans cette thèse, par la formalisation du corpus de connaissances issues d'expérimentations en milieu naturel, d'apporter une aide à la modélisation du comportement des incendies de forêt. Un prototype de système de gestion des connaissances est élaboré afin d'assister les scientifiques chargés de conduire des expérimentations en milieu naturel. Ce système de gestion des connaissances étant partie intégrante des outils informatiques à mettre en œuvre dans une zone atelier, nous nous permettrons d'imaginer ce que pourrait être une zone atelier pour la modélisation du comportement des incendies de forêt en France. La première partie de la thèse a pour objet de présenter le système incendie de forêt, la démarche de modélisation pour l'analyser ainsi que le recours à la démarche de formalisation de connaissance pour assister le modélisateur. La deuxième partie présente l'acquisition des connaissances dans le domaine de l'expérimentation en milieu naturel pour l'étude du comportement d'un incendie de forêt et leur formalisation à l'aide du langage de modélisation UML. La troisième partie présente, un prototype d'un système de gestion des connaissances issues d'expérimentations en milieu naturel : MODELLIS (MODELLed-Information System). Nous voyons comment celui-ci pourrait être intégré à ce que pourrait être une zone atelier pour l'étude du comportement des incendies de forêt dans le Sud de la France.