• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 51
  • 17
  • 2
  • Tagged with
  • 70
  • 70
  • 35
  • 35
  • 29
  • 20
  • 20
  • 19
  • 18
  • 17
  • 17
  • 16
  • 16
  • 13
  • 11
  • 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

Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité

Blanqui, Frédéric 13 July 2012 (has links) (PDF)
Dans ce document, nous montrons comment la notion de calculabilité introduite par W. W. Tait et étendue par Girard aux types polymorphes peut être utilisée et facilement étendue pour montrer la terminaison de différents types de relations de réécriture, y compris avec filtrage sur des symboles définis, filtrage d'ordre supérieur ou réécriture de classe modulo certaines théories équationnelles. Nous montrons également que la notion de clôture de calculabilité donne lieu a une relation bien fondée incluant l'extension à l'ordre supérieur par J.-P. Jouannaud et A. Rubio de l'ordre récursif sur les chemins de N. Dershowitz.
32

Modélisation de la sémantique lexicale dans le cadre de la théorie des types / Modelling lexical semantics in a type-theoretic framework

Mery, Bruno 05 July 2011 (has links)
Le présent manuscrit constitue la partie écrite du travail de thèse réalisé par Bruno Mery sous la direction de Christian Bassac et Christian Retoré entre 2006 et 2011, portant sur le sujet "Modélisation de la sémantique lexicale dans la théorie des types". Il s'agit d'une thèse d'informatique s'inscrivant dans le domaine du traitement automatique des langues, et visant à apporter un cadre formel pour la prise en compte, lors de l'analyse sémantique de la phrase, d'informations apportées par chacun des mots.Après avoir situé le sujet, cette thèse examine les nombreux travaux l'ayant précédée et s'inscrit dans la tradition du lexique génératif. Elle présente des exemples de phénomènes à traiter, et donne une proposition de système de calcul fondée sur la logique du second ordre. Elle examine ensuite la validité de cette proposition par rapport aux exemples et aux autres approches déjà formalisées, et relate une implémentation de ce système. Enfin, elle propose une brève discussion des sujets restant en suspens. / This paper is part of the thesis by Bruno Mery advised by Christian Bassac and Christian Retore in the years 2006-2011, on the topic "Modelling lexical semantics in a type-theoretic framework''. It is a doctoral thesis in computer science, in the area of natural language processing, aiming to bring forth a formal framework that takes into account, in the parsing of the semantics of a sentence, of lexical data.After a discussion of the topic, this thesis reviews the many works perceding it and adopts the tradition of the generative lexicon. It presents samples of data to account for, and gives a proposal for a calculus system based upon a second-order logic. It afterwards reviews the validity of this proposal, coming back to the data samples and the other formal approaches, and gives an implementation of that system. At last, it engages in a short discussion of the remaining questions.
33

Linéarité : un outil analytique pour l'étude de la complexité et de la sémantique des langages de programmation / Linearity : an analytic tool in the study of complexity and semantics of programming languages

Gaboardi, Marco 12 December 2007 (has links)
Dans la première partie, on propose un système de type pour le lambda-calcul, dans le style du calcul des séquents, nomme « Soft Type Assignment » (STA) qui est inspiré par la logique linéaire « soft ». STA a la propriété de réduction du sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on propose un déduction naturelle, STA_N. Ce système est simple mais il a le désavantage que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre ce problème, on propose le système STA_M, où les contextes sont des multi-ensembles, donc les règles pour renommer les variables peuvent être interdit. L’inférence de type pour STA_M ne semble pas décidable. On propose un algorithme qui pour chaque lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le terme soit type. Pi est correct et complet. Ensuite on étend le lambda-calcul par des constantes booléennes et on propose le système STA_B. La particularité de STA_B est que la règle du conditionnel utilise les contextes de façon additive. Chaque programme de STA_B peut être exécuté, par une machine abstraite, en espace polynomial. De plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose une restriction de PCF, nommée SlPCF. Ce langage est équipé avec une sémantique opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être interprèté en mode standard dans les espaces cohérents linéaires. SlPCF est complet pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract pour les espaces cohérents linéaires / In the first part, we propose, inspired by Soft Linear Logic, a type assignment system for lambda-calculus in sequent calculus style, named Soft Type Assignment (STA). STA enjoys the subject reduction property. and is correct and complete for polynomial time computations. Then, we propose a natural deduction named STA_N. While simple, STA_N has the disadvantage of allowing the explicit renaming of variables in the subject. To overcome to this problem, we propose another natural deduction system, named STA_M, where contexts are multisets, hence rules renaming variables can be avoided. The type inference for STA_M seems in general undecidable. We propose an algorithm Pi returning, for every lambda-term, a set of constraints that need to be satisfied in order to type the term. Pi is correct and complete. We extend the lambda-calculus by basic boolean constants and we propose the system STA_B. The peculiarity of STA_B is that the conditional rule treats the contexts in an additive way. Every STA_B program can be executed, through an abstract machine, in polynomial space. Moreover, STA_B is also complete for PSPACE. In the second part we propose a restriction of PCF, named SlPCF. The language is naturally equipped with an operational semantics mixing call-by-name and call-by-value parameter passing and it can be interpreted in linear coherence space in a standard way. SlPCF is recursive complete, but it is not complete, and thus not fully abstract, with respect to linear coherence spaces
34

Réalisabilité classique : nouveaux outils et applications / Classical realizability : new tools and applications

Geoffroy, Guillaume 29 March 2019 (has links)
La réalisabilité classique de Jean-Louis Krivine associe à chaque modèle de calcul et chaque modèle de la théorie des ensembles un nouveau modèle de la théorie des ensembles, appelé modèle de réalisabilité, d'une façon similaire au forcing. Chaque modèle de réalisabilité est muni d’une algèbre de Boole caractéristique $\gimel 2$ (gimel 2), dont la structure donne des informations sur les propriétés du modèle de réalisabilité. En particulier, les modèles de forcing correspondent au cas où $\gimel 2$ est l'algèbre de Boole à deux éléments.Ce travail présente de nouveaux outils pour manipuler les modèles de réalisabilité et donne de nouveaux résultats obtenus en les exploitant. L'un d'entre eux est qu'au premier ordre, la théorie des algèbres de Boole à au moins deux éléments est complète pour $\gimel 2$, au sens où $\gimel 2$ eut être rendue élémentairement équivalente à n'importe quelle algèbre de Boole. Deux autres résultats montrent que $\gimel 2$ peut être utilisée pour étudier les modèles dénotationnels de langage de programmation (chacun part d'un modèle dénotationnel et classifie ses degrés de parallélisme à l'aide de $\gimel 2$). Un autre résultat montre que la technique de Jean-Louis Krivine pour réaliser l'axiome des choix dépendants à partir de l'instruction quote peut se généraliser à des formes plus fortes de choix. Enfin, un dernier résultat, obtenu en collaboration avec Laura Fontanella, accompagne le précédent en adaptant la condition d'antichaîne dénombrable du forcing au cadre de la réalisabilité, ce qui semble semble ouvrir une piste prometteuse pour réaliser l'axiome du choix. / Jean-Louis Krivine's classical realizability defines, from any given model of computation and any given model of set theory, a new model of set theory called the realizability model, in a similar way to forcing. Each realizability model is equipped with a characteristic Boolean algebra $\gimel 2$ (gimel 2), whose structure encodes important information about the properties of the realizability model. For instance, forcing models are precisely the realizability models in which $\gimel 2$ is the Boolean algebra with to elements.This document defines new tools for studying realizability models and exploits them to derive new results. One such result is that, as far as first-order logic is concerned, the theory of Boolean algebras with at least two elements is complete for $\gimel 2$, meaning that for each Boolean algebra B (with at least two elements), there exists a realizability model in which $\gimel 2$ is elementarily equivalent to B. Next, two results show that $\gimel 2$ can be used as a tool to study denotational models of programming languages (each one of them takes a particular denotational model and classifies its degrees of parallelism using $\gimel 2$). Moving to set theory, another results generalizes Jean-Louis Krivine's technique of realizing the axiom of dependant choices using the instruction quote to higher forms of choice. Finally, a last result, which is joint work with Laura Fontanella, complements the previous one by adapting the countable antichain condition from forcing to classical realizability, which seems to open a new, promising approach to the problem of realizing the full axiom of choice.
35

SÉMANTIQUES ET SYNTAXES VECTORIELLES DE LA LOGIQUE LINÉAIRE

Tasson, Christine 04 December 2009 (has links) (PDF)
Avec les espaces de finitude, Ehrhard a exhibé une sémantique de la logique linéaire contenant une opération de différentiation. Dans ce cadre, l'interprétation des formules est décomposable en séries de Taylor. Cette étude a engendré des syntaxes différentielles. Cette thèse de sémantique dénotationnelle prolonge ce travail par une exploration de sémantiques vectorielles de la logique linéaire, et contribue à l'étude sémantique et syntaxique de la formule de Taylor. La première partie aborde la sémantique. Nous présentons l'interprétation des constructions de la logique linéaire dans les espaces vectoriels munis d'une topologie linéarisée, les espaces de Lefschetz. Nous définissons une notion intrinsèque d'espaces de finitude, les espaces de Lefschetz finitaires. Nous caractérisons les espaces de Lefschetz réflexifs complets à l'aide de bornologies linéaires. Enfin, nous montrons que la décomposition de Taylor reste valide dans ces espaces. La seconde partie porte sur les syntaxes différentielles. La formule de Taylor syntaxique traduit un terme en une superposition de termes différentiels qui sont autant de possibilités d'exécutions. Comme l'ont montré Ehrhard et Regnier, les termes issus de cette traduction vérifient une relation de cohérence. Nous introduisons une sémantique totale qui capture cette relation. Puis, nous construisons une extension vectorielle du lambda-calcul, le calcul barycentrique, interprété par cette sémantique totale. Enfin, dans le cadre des réseaux différentiels, nous présentons un algorithme non déterministe qui permet de décider si un ensemble fini de réseaux différentiels provient de la traduction d'un réseau de la logique linéaire par la formule de Taylor syntaxique.
36

Etude d'un $\lambda$-calcul issu d'une logique classique

Saber, Khelifa 06 July 2007 (has links) (PDF)
Le $\lambda \mu^{\wedge \vee}$-calcul est une extension du $\lambda$-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs.<br>Les principaux résultats de cette thèse sont :<br>- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.<br>- Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures.<br>- Une sémantique de réalisabilité pour le $\lambda \mu^{\wedge \vee}$-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos.<br>- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.<br>- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent.
37

Géométrie de l'Interaction et Réseaux Différentiels

De Falco, Marc 28 May 2009 (has links) (PDF)
La Géométrie de l'Interaction (GdI) de Girard est une sémantique des langage de programmations tenant compte de leur dynamique de réduction.<br />Dans un premier temps, on présente les réseaux d'interaction de Lafont comme une instance particulière de GdI. Puis, on définis un cadre général d'étude de la GdI à partir d'un ensemble de symboles et de règles d'interaction.<br />Dans un second temps, on introduit une notion de concision associée à la GdI et on montre dans quelle mesure cette notion fait du sens à l'aide d'une famille d'exemple basée sur les entiers de Church.<br />Dans un dernier temps, on présente les réseaux d'interaction différentiels d'Ehrhard et Regnier et on définit leur GdI. On montre que la théorie usuelle de Danos-Regnier est entièrement récupérée.
38

Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes

Herbelin, Hugo 23 January 1995 (has links) (PDF)
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en « l'élimination des coupures ». Deux interprétations sont considérées.<br /><br />Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.<br /><br />La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.<br /><br />Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.<br /><br />Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.
39

Sur la notion d'observation en sémantique

Leperchey, Benjamin 09 December 2005 (has links) (PDF)
Cette thèse présente différentes notions d'observation en sémantique, et quelques résultats sur leurs relations. Après avoir rappelé les définitions du lambda-calcul simplement typé et de ses modèles, nous présentons la notion d'observation définie par un modèle. Dans une première partie, nous présentons les liens entre cette notion et la définissabilité relative, en prenant les exemples de PCF unaire, de PCF finitaire et du modèle fortement stable de PCF, en étendant des travaux de Bucciarelli, Malacaria et Longley.<br />La partie suivante est consacrée à l'étude de la notion d'observation dans le cadre d'un langage avec des effets de bord. Nous proposons un modèle basé sur les domaines de Fraenkel-Mostowski, sur lequel nous définissons des relations logiques pour prouver des équivalences, aui servent à distinguer la partie publique de la mémoire de la partie secrète où les invariants sont préservés; ce qui établit un lien avec les problématiques de sécurité.<br />Enfin, nous étudions la question du temps d'exécution en sémantique dénotationnelle. Nous proposons une construction axiomatique, basée sur une monade, pour représenter le te,ps d'exécution sans le rendre observable par le contexte. Nous appliquons cette construction au modèle des espaces de cohérence et aux jeux de Hyland et Ong. Nous prouvons que ce dernier modèle est complètement adéquat.
40

Récursion généralisée et inférence de types avec intersection

ZIMMER, Pascal 29 April 2004 (has links) (PDF)
Dans une première partie, nous définissons un nouveau langage à base fonctionnelle et avec récursion généralisée, en utilisant le système de types avec degrés de Boudol pour éliminer les récursions dangereuses. Ce langage est ensuite étendu par des enregistrements récursifs, puis par des mixins, permettant ainsi de mêler totalement les paradigmes fonctionnels et objets. Nous présentons également une implémentation, MlObj, ainsi que la machine abstraite servant à son exécution.<br /><br />Dans une deuxième partie, nous présentons un nouvel algorithme d'inférence pour les systèmes de types avec intersection, dans le cadre d'une extension du lambda-calcul. Après avoir prouvé sa correction, nous étudions sa généralisation aux références et à la récursion, nous le comparons aux algorithmes d'inférence déjà existants, notamment à celui de Système I, et nous montrons qu'il devient décidable à rang fini.

Page generated in 0.0488 seconds