Prouver l’équivalence de programmes écrits dans un langage fonctionnel avec références est un problème notoirement difficile. L’objectif de cette thèse est de proposer un système logique dans lequel de telles preuves peuvent être formalisées, et dans certains cas inférées automatiquement. Dans la première partie, une méthode générique d’extension de la théorie des types dépendants est proposée, basée sur une interprétation du forcing vu comme une traduction de préfaisceaux de la théorie des types. Cette extension dote la théorie des types de constructions récursives gardées, qui sont utilisées ensuite pour raisonner sur les références d’ordre supérieure. Dans une deuxième partie, nous définissons une sémantique des jeux nominale opérationnelle pour un langage avec références d’ordre supérieur. Elle marie la structure catégorique de la sémantique des jeux avec une représentation sous forme de traces de la dénotation des programmes, qui se calcule de manière opérationnelle et dispose donc de bonnes propriétés de modularité. Cette sémantique nous permet ensuite de prouver la complétude de relations logiques à la Kripke définit de manière directe, via l’utilisation de types récursifs gardés, sans utilisation de la biorthogonalité. Une telle définition directe nécessite l’utilisation de mondes omniscient et un contrôle fin des locations divulguées. Finalement, nous introduisons une logique temporelle qui donne un cadre pour définir ces relations logiques à la Kripke. Nous ramenons alors le problème de l’équivalence contextuelle à la satisfiabilité d’une formule de cette logique générée automatique, c’est à dire à l’existence d’un monde validant cette formule. Sous certaines conditions, cette satisfiabilité peut être décidée via l’utilisation d’un solveur SMT. La complétude de notre méthode devrait permettre d’obtenir des résultats de décidabilité pour l’équivalence contextuelle de certains fragment du langage considéré, en fournissant un algorithme pour construire de tels mondes. / Proving program equivalence for a functional language with references is a notoriously difficult problem. The goal of this thesis is to propose a logical system in which such proofs can be formalized, and in some cases inferred automatically. In the first part, a generic extension method of dependent type theory is proposed, based on a forcing interpretation seen as a presheaf translation of type theory. This extension equips type theory with guarded recursive constructions, which are subsequently used to reason on higher-order references. In the second part, we define a nominal game semantics for a language with higher-order references. It marries the categorical structure of game semantics with a trace representation of denotations of programs, which can be computed operationally and thus have good modularity properties. Using this semantics, we can prove the completeness of Kripke logical relations defined in a direct way, using guarded recursive types, without using biorthogonality. Such a direct definition requires omniscient worlds and a fine control of disclosed locations. Finally, we introduce a temporal logic which gives a framework to define these Kripke logical relations. The problem of contextual equivalence is then reduced to the satisfiability of an automatically generated formula defined in this logic, i.e. to the existence of a world validating this formula. Under some conditions, this satisfiability can be decided using a SMT solver. Completeness of our methods opens the possibility of getting decidability results of contextual equivalence for some fragments of the language, by giving an algorithm to build such worlds.

Le thème général de cette thèse est l’exploitation de l’interaction entre la sémantique dénotationnelle et la syntaxe. Des sémantiques satisfaisantes ont été découvertes pour les preuves en logique intuitionniste et linéaire, mais dans le cas de la logique classique, la solution du problème est connue pour être particulièrement difficile. Ce travail commence par l’étude d’une interprétation concrète des preuves classiques dans la catégorie des ensembles ordonnés et bimodules, qui mène à l’extraction d’invariants significatifs. Suit une généralisation de cette sémantique concrète, soit l’interprétation des preuves classiques dans une catégorie compacte fermée où chaque objet est doté d’une structure d’algèbre de Frobenius. Ceci nous mène à une définition de réseaux de démonstrations pour la logique classique. Le concept de correction, l’élimination des coupures et le problème de la “full completeness” sont abordés au moyen d’un enrichissement naturel dans les ordres sur la catégorie de Frobenius, produisant une catégorie pour l'élimination des coupures et un concept de ressources pour la logique classique. Revenant sur notre première sémantique concrète, nous montrons que nous avons une représentation fidèle de la catégorie de Frobenius dans la catégorie des ensembles ordonnés et bimodules. / The general theme of this thesis is the exploitation of the fruitful interaction between denotational semantics and syntax. Satisfying semantics have been discovered for proofs in intuitionistic and certain linear logics, but for the classical case, solving the problem is notoriously difficult.This work begins with investigations of concrete interpretations of classical proofs in the category of posets and bimodules, resulting in the definition of meaningful invariants of proofs. Then, generalizing this concrete semantics, classical proofs are interpreted in a free symmetric compact closed category where each object is endowed with the structure of a Frobenius algebra. The generalization paves a way for a theory of proof nets for classical proofs. Correctness, cut elimination and the issue of full completeness are addressed through natural order enrichments defined on the Frobenius category, yielding a category with cut elimination and a concept of resources in classical logic. Revisiting our initial concrete semantics, we show we have a faithful representation of the Frobenius category in the category of posets and bimodules.

Les substitutions explicites ont été introduites comme un raffinement du lambda-calcul, celui-ci étant le<br />formalisme utilisé pour étudier la sémantique des langages de programmation. L'objet de cette thèse<br />est l'étude de leurs propriétés de normalisation forte et de préservation de la normalisation forte. Ce<br />manuscrit rend compte de plusieurs travaux autour de ces propriétés de normalisation, regroupés en<br />trois volets.<br /><br />Le premier d'entre eux formalise une technique générale de preuve de normalisation forte utilisant<br />la préservation de la normalisation forte. On applique cette technique à un spectre assez large de calculs<br />avec substitutions explicites afin de mesurer les limites de son utilisation. Grâce à cette technique, on<br />prouve un résultat nouveau : la normalisation forte du lambda-upsilon-calcul simplement typé.<br /><br />Le deuxième travail est l'étude de la normalisation d'un calcul symétrique non-déterministe issu de<br />la logique classique formulée dans le calcul des séquents, auquel est ajouté des substitutions explicites.<br />La conjonction des problèmes posés par les calculs symétriques et ceux posés par les substitutions<br />explicites semble vouer à l'échec l'utilisation de preuves par réductibilité. On utilise alors la technique<br />formalisée dans le premier travail, ce qui nous demande de prouver tout d'abord la préservation de la<br />normalisation forte. A cette fin, on utilise un fragment de la théorie de la perpétuité dans les systèmes<br />de réécriture.<br /><br />La définition d'une nouvelle version du lambda-ws-calcul avec nom, le lambda-wsn-calcul, constitue le troisième<br />volet de la thèse. Pour prouver sa normalisation forte par traduction et simulation dans les réseaux<br />de preuve, on enrichit l'élimination des coupures de ceux-ci avec une nouvelle règle, ce qui nous oblige<br />à prouver que cette nouvelle notion de réduction est fortement normalisante.

Cette thèse se situe dans le cadre de la synthèse logique. Elle a pour objet la synthèse logique optimisée de circuits sur réseaux programmables à base de «tables de vérité» de type «Xilinx». Ces réseaux programmables ont été à l'origine du premier succès commercial des réseaux reprogrammables à faible granularité. Une première solution pratiquée industriellement a consisté à associer une bibliothèque équivalente de primitives logiques simples de type «cellule standard» à un réseau Xilinx. Une telle approche conduit à une très pauvre utilisation de la technologie cible car elle ne tire pas profit de la richesse de la cellule de base. Cette thèse s'intéresse, en conséquence, à des approches plus ciblées. Il s'agit de décomposer de façon optimisée les parties combinatoires en sous-fonctions «saturant» les possibilités des cellules élémentaires. Pour ceci, le traitement des fonctions booléennes sera effectué dès l'étape de factorisation en fonction du but final. Après un rappel de la factorisation «lexicographique», qui a comme fondement l'existence d'un ordonnancement des entrées, une méthode de décomposition en sous fonctions de k variables est proposée. Elle sert de base à des méthodes de décomposition technologique pour les séries Xilinx 3000 et Xilinx 4000. Deux alternatives à cette factorisation lexicographique sont proposées, une factorisation utilisant une représentation par diagramme de décision binaire (ROBDD) et une factorisation algébrique classique adaptée aux caractéristiques de la cible Xilinx. La dernière étape de synthèse concerne de façon plus fine le regroupement des sous-fonctions dans la cellule physique Xilinx et se préoccupe de l'optimisation des points de mémorisation, des buffers et des ressources d'horloge. Une évaluation sur un ensemble d'exemples internationaux et industriels démontre l'efficacité des méthodes proposées. Ce travail a fait l'objet d'un transfert technologique vers le logiciel industriel ASYL+

La définition d'un modèle d'évaluation est le problème clé d'un système de recherche d'informations. De nombreux modelés existent, qui sont généralement spécifiques a un type d'application particulier et avec lesquels la prise en compte de la sémantique est difficile. Dans la première partie de cette thèse, nous dégageons d'abord deux critères pour la valuation de la correspondance entre un document et une requête: l'exhaustivité et la spécificité du document pour la requête. Nous définissons ensuite un modèle général fonde sur la logique modale floue pour la valuation des deux critères. Ce modèle est compare avec quelques modèles existants pour démontrer sa généralité. Dans la seconde partie de la thèse, le modèle propose est applique au processus d'interrogation du prototype rime pour la recherche d'informations médicales. Ce prototype possède une interface en langue quasi naturelle (un sous-ensemble du français). Un processus d'interrogation se décompose en deux parties: l'interprétation des requêtes en langue quasi naturelle et l'évaluation des requêtes en utilisant le modèle général précédemment défini. Ces deux parties sont étudiées en détail. Une réalisation est finalement présentée, ainsi que son expérimentation sur un corpus médical

La formalisation du principe de rationalité dans la plupart des modèles d'agent permet rarement de spécifier complètement les réactions du système. C'est pourquoi nous considérons dans cette thèse l'introduction d'une phase de décision explicite au sein de ces modèles. Plus précisément, nous proposons une nouvelle façon entièrement qualitative de représenter les informations sur la désirabilité des alternatives nécessaires à cette phase : les préférences. Cette dernière est formalisée en logique des prédicats du premier ordre.<br /><br />Afin d'autoriser une spécification intuitive des préférences, nous supposons que les informations "initiales" sont des comparaisons entres des propriétés que peuvent vérifier les différentes alternatives. Ces comparaisons vérifient les principes d'expansion, de transitivité, et de Ceteris Paribus. De plus, elles sont spécifiées par points de vue éventuellement contradictoires et telles que deux propriétés quelconques sont jugées indifférentes par défaut.<br />Afin de départager un grand nombre d'alternatives et en particulier pour dépasser une limite de l'hypothèse Ceteris Paribus, nous proposons d'étendre ces informations via une phase dite "d'extension" en considérant chaque préférence (dite "primitive") comme un argument pour départager les alternatives.<br />Afin de gérer les contradictions entre points de vue, nous formalisons l'introduction d'une étape dite "d'agrégation". Cette dernière permet, via un mécanisme d'élection, de générer une unique préférence "globale".<br /><br />Enfin, nous proposons une voie pour intégrer notre travail au modèle logique d'agent rationnel proposée par Sadek ainsi qu'une manière pour utiliser nos préférences conjointement avec d'autres types d'informations sur la désirabilité.

Ce travail présente une approche générale du traitement de l'intégrité sémantique des données gérées par les systèmes de gestion de bases de données. Une organisation des connaissances (lois générales, données, etc.) d'une réalité/environnement est également présentée, accompagnée d'une méthode permettant leur définition cohérente. Les idées proposées ont été formalisées au moyen du calcul des prédicats du 1(e)r ordre puis mises en œuvre par l'intermédiaire du langage Prolog.

L'objectif principal de cette thèse est de définir un langage logique de haut niveau qui permet l'expression de politiques de sécurité complexes au sein d'un modèle de contrôle d'accès. Le développement de ce langage se fait en trois temps. Dans un premier temps nous présentons un modèle dynamique basé sur les rôles. Ainsi, nous considérons que l'évolution de l'état de sécurité d'un service dépend de l'exécution de ses fonctionnalités. Dans un deuxième temps nous définissons un formalisme basé sur les attributs qui offre plus de flexibilité en termes de spécifications des conditions de contrôle d'accès, et ajoutons la notion de workflow qui permet de modéliser le comportement d'un service. Dans un dernier temps, nous ajoutons un mécanisme de négociation qui permet à chaque service de définir sa propre politique d'échange avec les autres services dans l'environnement. La conception d'un tel cadre logique unifié facilite l'analyse de sûreté des politiques de sécurité puisque tous les facteurs qui influencent les décisions de contrôle d'accès sont pris en compte dans le même cadre. Ainsi le second objectif de cette thèse est d'étudier d'une part les principales propriétés de contrôle d'accès tels la délégation et la séparation des tâches et d'autre part les propriétés de sécurité pour la communication entre les différents services au niveau de la négociation.

Reproduction de : Thèse de doctorat : Informatique : Orléans : 1995. / Résumé en français. Bibliogr. p. 264-270.

Malgré sa condamnation post-positiviste et sa réception négative par la gauche, l’empirisme logique regagne en intérêt. Cette thèse est une contribution à la littérature émergente du «Cercle de Vienne de gauche» (CVG). Autour de Neurath et quelques autres personnalités de l’aile gauche du Cercle (Carnap, Frank, Hahn, Zilsel), nous proposons de repenser la relation de l’empirisme logique avec le marxisme. Ces deux courants se rejoignent dans leur défense d’une «conception scientifique du monde» et leur sécularisme radical. Les critiques communistes et néo-marxistes (l’École de Francfort, l’épistémologie féministe) adressées à l’empirisme logique sont recensées et leur pertinence questionnée à travers les données de l’historiographie du CVG. La politique de l’empirisme logique est examinée à travers les textes économiques de Neurath et son œuvre d’infographiste. Son engagement pour l’économie socialiste planifiée et ses efforts en graphisme pour la popularisation des méthodes quantitatives (la méthode Isotype pour la visualisation des statistiques sociales) sont présentés en vue d’une évaluation politique du CVG, ainsi que les connexions de l’empirisme logique avec le mouvement pour une langue auxiliaire internationale. / Despite logical empiricism’s dismissal by ambient postpositivism in academia as well as by the Far Left, a growing interest in its previously unknown socialist origins has resulted in a new topic in the history of philosophy of science : «Left Vienna Circle» (LVC). This thesis dedicated to LVC studies aims to clarify the politics of European logical empiricism. A presentation of its major critics from the Left (from communist parties to neo-Marxist trends like Frankfurt School and feminist epistemology) is followed by more recent arguments about its socialist politics. The «scientific world conceptions» of logical empiricism and Marxism will be compared through the work of Neurath and some other representatives of LVC (Carnap, Frank, Zilsel, Hahn). Alongside the connections of logical empiricism to the movement for an international auxiliary language, Neurath’s economical writings and his efforts to popularize quantitative methods in social sciences (the Isotype method of visual statistics) will be presented in an attempt to evaluate the politics of logical empiricism.