• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 25
  • 14
  • 2
  • Tagged with
  • 41
  • 41
  • 20
  • 20
  • 17
  • 16
  • 14
  • 14
  • 13
  • 12
  • 11
  • 10
  • 10
  • 10
  • 9
  • 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.
1

Programmer, calculer et raisonner avec les réseaux de la Logique Linéaire

Gimenez, Stéphane 16 December 2009 (has links) (PDF)
La première partie propose divers systèmes de réseaux d'interaction (calcul par réécriture muni d'une réduction atomique, locale et parallèle) qui simulent l'exécution des preuves de la logique linéaire (considérées comme des programmes). Les différents fragments de cette logique sont abordés, on y ajoute aussi une récursion pour atteindre l'expressivité des langages de programmation usuels. Ce procédé de simulation permet d'exécuter certains langages à l'aide d'une petite machine d'exécution multi-processeurs. Il s'appuie sur des représentations localisées de boîtes issues des réseaux de preuve ; certaines utilisent avantageusement un canal de contrôle pour ne rien perdre de la structure des preuves représentées. La deuxième partie s'articule autour de la logique linéaire différentielle et de ses ressources à usage unique. On la munit d'une super-promotion, qui se distingue notamment d'une promotion ordinaire parce qu'elle préserve la symétrie originelle de ce formalisme. C'est la pendante côté logique de la réplication qu'on trouve parfois dans les algèbres de processus. On arrive à isoler l'un de ses composants plus primitifs, le co-enfouissement, responsable de leur dynamique incontrôlée (pour l'instant). Cette construction peut être exprimée dans la syntaxe du λ-calcul avec ressources ou dans un système de réseaux. La séquentialisation de ces derniers requiert une présentation originale de la logique, fondée sur un calcul de structures, et qui a potentiellement d'autres intérêts. Il est aussi question de réalisabilité pour les systèmes différentiels et de sémantique relationnelle pour les divers réseaux présentés.
2

λ-calcul différentiel et logique classique : interactions calculatoires

Vaux, Lionel 23 November 2007 (has links) (PDF)
Cette thèse de théorie de la démonstration étudie les interactions entre le λ-calcul différentiel d'Ehrhard et Regnier d'un côté, et certaines émanations calculatoires de la logique classique (le λμ-calcul de Parigot et le λ-barre-μ-calcul de Herbelin) de l'autre. L'étude est initiée et guidée par la décomposition de ces calculs dans des extensions de la logique linéaire de Girard.<br /><br />Dans une première partie, on définit un cadre commun pour ces extensions, dans le formalisme des réseaux d'interaction de Lafont, et on y rappelle des résultats de la littérature ou du folklore. On donne en particulier la traduction du λμ-calcul et du λ-barre-μ-calcul dans les réseaux polarisés de Laurent et celle du fragment finitaire du λ-calcul différentiel dans les réseaux différentiels d'Ehrhard et Regnier.<br /><br />Dans la deuxième partie, on introduit les réseaux différentiels polarisés (RDP), comme l'extension par une polarisation à la Laurent des réseaux différentiels. La pertinence des règles de réduction nouvelles est soulignée par l'étude d'un modèle dénotationnel commun aux réseaux différentiels et aux réseaux polarisés.<br /><br />Enfin, on présente trois calculs de termes, chacun pouvant être considéré comme une lecture en arrière de tout ou partie des interactions définies par les RDP : un λμ-calcul différentiel, qui correspond à la réunion des réseaux différentiels et des réseaux polarisés ; un λ-barre-μ-calcul avec produit de convolution sur les piles, qui fait intervenir la structure de bigèbre des types polarisés introduite dans les RDP, mais pas la dérivée ; enfin, un λ-barre-μ-calcul différentiel qui développe toute l'expressivité des RDP.
3

Reflexive spaces of smooth functions : a logical account of linear partial differential equations / Espaces réflexifs de fonctions lisses : un compte rendu logique des équations aux dérivées partielles linéaires

Kerjean, Marie 19 October 2018 (has links)
La théorie de la preuve se développe depuis la correspondance de Curry-Howard suivant deux sources d’inspirations : les langages de programmation, pour lesquels elle agit comme une théorie des types de données, et l’étude sémantique des preuves. Cette dernière consiste à donner des modèles mathématiques pour les comportements des preuves/programmes. En particulier, la sémantique dénotationnelle s’attache à interpréter les deux-ci comme des fonctions entre des types, et permet en retour d’affiner notre compréhension des preuves/programmes. La logique linéaire (LL), introduite par Girard, donne une interprétation logique des notions d’algèbre linéaire, quand la logique linéaire différentielle (DiLL), introduite par Ehrhard et Regnier, permet une compréhension logique de la notion de différentielle.Cette thèse s’attache à renforcer la correspondance sémantique entre théorie de la preuve et analyse fonctionnelle, en insistant sur le caractère involutif de la négation dans DiLL.La première partie consiste en un rappel des notions de linéarité, polarisation et différentiation en théorie de la preuve, ainsi qu’un exposé rapide de théorie des espaces vectoriels topologiques. La deuxième partie donne deux modèles duaux de la logique linéaire différentielle, interprétant la négation d’une formule respectivement par le dual faible et le dual de Mackey. Quand la topologie faible ne permet qu’une interprétation discrète des preuves sous forme de série formelle, la topologie de Mackey nous permet de donner un modèle polarisé et lisse de DiLL, et de raffiner des résultats précédemment obtenus par Blute, Dabrowski, Ehrhard et Tasson. Enfin, la troisième partie de cette thèse s’attache à interpréter les preuves de DiLL par des distributions à support compact. Nous donnons un modèle polarisé de DiLL où les formules négatives sont interprétés par des espaces Fréchet Nucléaires. Nous montrons que enfin la résolution des équations aux dérivées partielles linéaires à coefficients constants obéit à une syntaxe qui généralise celle de DiLL, que nous détaillons. / Around the curry-coward correspondence, proof-theory has grown along two distinct fields : the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions from/of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation. This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in a quick overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two classic topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fréchet Nuclear spaces, and proofs are distributions with compact support. We also show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.
4

Réseaux et séquents ordonnés

Retoré, Christian 26 February 1993 (has links) (PDF)
Cette thèse présente un calcul des séquents pour la logique linéaire enrichie d'un connecteur non commutatif et autodual "précède" situé entre le "par" et le "tenseur". Il est défini pour des séquents dont les formules sont orientées par un ordre partiel. Un calcul de réseaux de démonstration quotientant ce calcul des séquents est défini en termes de graphes orientés. Ce calcul est doté d'une sémantique dénotationnelle dans les espaces cohérents, préservée par élimination des coupures, un processus convergent et confluent. Des résultats combinatoires nécessaires sur les ordres partiels et sur la structure des graphes de démonstrations sont établies ainsi que quelques propriétés du calcul commutatif avec la règle MIX.
5

Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire

Laurent, Olivier 05 February 2010 (has links) (PDF)
La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.
6

Sharing, Superposition and Epansion : Geometrical Studies on the semantics and Implementation of lambda-calculi and proof-nets / Partage, superposition et développement : Etudes géométriques sur la sémantique et l'implémentation de lambda-calculs et de réseaux de preuves

Solieri, Marco 30 November 2016 (has links)
Des sémantiques élégantes et des implémentations efficaces des langages de programmation fonctionnels peuvent être décrits par les mêmes structures mathématiques, notamment dans la correspondance Curry-Howard, où le programmes, les types et l’exécution, coïncident aux preuves, formules et normalisation. Une telle flexibilité est aiguisé par l’approche déconstructive et géométrique de la logique linéaire (LL) et les réseaux de preuve, et de la réduction optimale et les graphes de partage (SG).En adaptent la géométrie de l’interaction de Girard, cette thèse propose une géométrie de l’interaction des ressources (GoRI), une sémantique dynamique et dénotationnelle, qui décrit algébriquement par leurs chemins, les termes du calcul des ressources (RC), une variation linéaire et non-déterministe du lambda calcul (LC). Les séries infinis dans RC sont aussi le domaine du développement de Taylor-Ehrhard-Regnier, une linéarisation du LC. La thèse explique la relation entre ce dernier et la réduction démontrant qu’ils commutent, et présente une version développé de la formule d’exécution pour calculer les chemins du LC typé.Les SG sont un modèle d’implémentation du LC, dont les pas sont locales et asynchrones, et le partage implique et les termes et les contextes. Bien que les tests ont montré des accélérations exceptionnelles, jusqu à exponentielles, par rapport aux implémentations traditionnelles, les SG n’ont pas que des avantages. La thèse montre que, dans le cas restreint des réseaux élémentaires, où seule le cœur des SG est requis, les désavantages sont au plus quadratique, donc inoffensifs. / Elegant semantics and efficient implementations of functional programming languages can both be described by the very same mathematical structures, most prominently with in the Curry-Howard correspondence, where programs, types and execution respectively coincide with proofs, formulæ and normalisation. Such a flexibility is sharpened by the deconstructive and geometrical approach pioneered by linear logic (LL) and proof-nets, and by Lévy-optimal reduction and sharing graphs (SG).Adapting Girard’s geometry of interaction, this thesis introduces the geometry of resource interaction (GoRI), a dynamic and denotational semantics, which describes, algebra-ically by their paths, terms of the resource calculus (RC), a linear and non-deterministic variation of the ordinary lambda calculus. Infinite series of RC-terms are also the domain of the Taylor-Ehrhard-Regnier expansion, a linearisation of LC. The thesis explains the relation between the former and the reduction by proving that they commute, and provides an expanded version of the execution formula to compute paths for the typed LC. SG are an abstract implementation of LC and proof-nets whose steps are local and asynchronous, and sharing involves both terms and contexts. Whilst experimental tests on SG show outstanding speedups, up to exponential, with respect to traditional implementations, sharing comes at price. The thesis proves that, in the restricted case of elementary proof-nets, where only the core of SG is needed, such a price is at most quadratic, hence harmless. / Semantiche eleganti ed implementazioni efficienti di linguaggi di programmazione funzionale possono entrambe essere descritte dalle stesse strutture matematiche, più notevolmente nella corrispondenza Curry-Howard, dove i programmi, i tipi e l’esecuzione coincidono, nell’ordine, con le dimostrazioni, le formule e la normalizzazione. Tale flsesibilità è acuita dall’approccio decostruttivo e geometrico della logica lineare (LL) e le reti di dimostrazione, e della riduzione ottimale e i grafi di condivisione (SG).Adattando la geometria dell’interazione di Girard, questa tesi introduce la geometria dell’interazione delle risorse (GoRI), una semantica dinamica e denotazionale che descrive, algebricamente tramite i loro per-corsi, i termini del calcolo delle risorse (RC), una variante lineare e non-deterministica del lambda calcolo ordinario. Le serie infinite di termini del RC sono inoltre il dominio dell’espansione di Taylor-Ehrhard-Regnier, una linearizzazione del LC. La tesi spiega la relazione tra quest’ultima e la riduzione dimostrando che esse commutano, e fornisce una versione espansa della for-mula di esecuzione per calcolare i percorsi del LC tipato. I SG sono un modello d’implementazione del LC, i cui passi sono loc-ali e asincroni, e la cui condivisione riguarda sia termini che contesti. Sebbene le prove sperimentali sui SG mostrino accellerazioni eccezionali, persino esponenziali, rispetto alle implementazioni tradizionali, la condivisione ha un costo. La tesi dimostra che, nel caso ristretto delle reti elementari, dove è necessario solo il cuore dei SG, tale costo è al più quad-ratico, e quindi innocuo.
7

Concurrency, references and linear logic / Concurrences, Références et Logique Linéaire

Hamdaoui, Yann 25 September 2018 (has links)
Le sujet de cette thèse est l’étude de l’encodage des références et de la concurrence dans la Logique Linéaire. Notre motivation est de montrer que la Logique Linéaire est capable d’encoder des effets de bords, et pourrait ainsi servir comme une cible de compilation pour des langages fonctionnels qui soit à la fois viable, formalisée et largement étudiée. La notion clé développée dans cette thèse est celle de zone de routage. C’est une famille de réseaux de preuve qui correspond à un fragment de la logique linéaire différentielle, et permet d’implémenter différentes primitives de communication. Nous les définissons et étudions leur théorie. Nous illustrons ensuite leur expressivité en traduisant un λ-calcul avec concurrence, références et réplication dans un fragment des réseaux différentiels. Pour ce faire, nous introduisons un langage semblable au λ-calcul concurrent d’Amadio, mais avec des substitutions explicites à la fois pour les variables et pour les références. Nous munissons ce langage d’un système de types et d’effets, et prouvons la normalisation forte des termes bien typés avec une technique qui combine la réductibilité et une nouvelle technique interactive. Ce langage nous permet de prouver un théorème de simulation, et un théorème d’adéquation pour la traduction proposée. / The topic of this thesis is the study of the encoding of references andconcurrency in Linear Logic. Our perspective is to demonstrate the capabilityof Linear Logic to encode side-effects to make it a viable, formalized and wellstudied compilation target for functional languages in the future. The keynotion we develop is that of routing areas: a family of proof nets whichcorrespond to a fragment of differential linear logic and which implementscommunication primitives. We develop routing areas as a parametrizable deviceand study their theory. We then illustrate their expressivity by translating aconcurrent λ-calculus featuring concurrency, references and replication to afragment of differential nets. To this purpose, we introduce a language akin toAmadio’s concurrent λ-calculus, but with explicit substitutions for bothvariables and references. We endow this language with a type and effect systemand we prove termination of well-typed terms by a mix of reducibility and anew interactive technique. This intermediate language allows us to prove asimulation and an adequacy theorem for the translation
8

Sémantique des jeux asynchrones et réécriture 2-dimensionnelle

Mimram, Samuel 01 December 2008 (has links) (PDF)
Les sémantiques de jeux s'attachent à caractériser le comportement interactif des preuves et des programmes, en les modélisant par des stratégies qui décrivent la façon dont ils réagissent à leur environnement. Afin de prendre en compte les aspects concurrents des preuves en logique linéaire, nous avons été amenés à retravailler les notions et techniques classiques de sémantique des jeux pour les étendre à un cadre asynchrone et non-alterné. Dans une première partie, nous définissons une famille de stratégies asynchrones donnant lieu à un modèle de logique linéaire, pleinement complet pour le fragment multiplicatif. Ces stratégies sont définies de façon locale par une série d'axiomes diagrammatiques ; elles sont ensuite raffinées par un critère dynamique d'ordonnancement, dont nous montrons qu'il impose une version orientée du critère de correction des réseaux de preuve. Cette formulation asynchrone permet d'unifier des modèles variés de la logique linéaire - aussi bien séquentiels que concurrents, dynamiques que statiques - où les preuves sont vues comme des stratégies séquentielles, des stratégies concurrentes, des relations ou des structures d'événements. Dans une seconde partie, nous abordons une autre approche pour décrire la causalité induite par les preuves et introduisons une sémantique de jeux capturant les dépendances engendrées par les connecteurs du premier ordre en logique propositionnelle. Nous montrons que la catégorie résultante peut être finiment présentée par un 2-polygraphe et étudions la possibilité d'orienter cette présentation en un système de réécriture confluent, notamment en introduisant un algorithme d'unification dans ce cadre 2-dimensionnel.
9

Logique dans le Facteur Hyperfini: Géométrie de l'Interaction et Complexité

Seiller, Thomas 13 November 2012 (has links) (PDF)
Cette thèse est une étude de la géométrie de l'interaction dans le facteur hyperfini (GdI5), introduite par Jean-Yves Girard, et de ses liens avec les constructions plus anciennes. Nous commençons par montrer comment obtenir des adjonctions purement géométriques comme une identité entre des ensembles de cycles apparaissant entre des graphes. Il est alors possible, en choisis- sant une fonction qui mesure les cycles, d'obtenir une adjonction numérique. Nous montrons ensuite comment construire, sur la base d'une adjonction numérique, une géométrie de l'interaction pour la logique linéaire multiplicative additive où les preuves sont interprétées par des graphes. Nous expliquons également comment cette construction permet de définir une sémantique dénotationnelle de MALL, et une notion de vérité. Nous étudions finalement une généralisation de ce cadre utilisant des outils de théorie de la mesure afin d'interpréter les exponentielles et le second ordre. Les constructions sur les graphes étant paramétrées par une fonction de mesure des cycles, nous entreprenons ensuite l'étude de deux cas particuliers. Le premier s'avère être une version combinatoire de la GdI5, et nous obtenons donc une interprétation géométrique de l'orthogonalité basée sur le déterminant de Fuglede-Kadison. Le second cas particulier est une version combinatoire des constructions plus anciennes de la géométrie de l'interaction, où l'orthogonalité est basée sur la nilpotence. Ceci permet donc de comprendre le lien entre les différentes versions de la géométrie de l'interaction, et d'en déduire que les deux adjonctions -- qui semblent à première vue si différentes -- sont des conséquences d'une même identité géométrique. Nous étudions ensuite la notion de vérité subjective. Nous commençons par considérer une version légè- rement modifiée de la GdI5 avec une notion de vérité dépendant du choix d'une sous-algèbre maximale commutative (masa). Nous montrons qu'il existe une correspondance entre la classification des masas introduite par Dixmier (regulière, semi-régulière, singulière) et les fragments de la logique linéaire que l'on peut interpréter dans cette géométrie de l'interaction. Nous étudions alors la vérité subjective de la GdI5, qui dépends du choix d'une représentation du facteur hyperfini de type II1, à la lumière de ce résultat. Finalement, nous détaillerons une proposition de Girard pour étudier les classes de complexité et dé- taillons la caractérisation obtenue par ce dernier de la classe de complexité co-NL, en montrant comment coder un problème complet pour cette classe à l'aide d'opérateurs.
10

Étude de la polarisation en logique

Laurent, Olivier 11 March 2002 (has links) (PDF)
Issue des travaux sur la logique linéaire et l'analyse calculatoire de la logique classique, la notion de polarités semble jouer un rôle essentiel dans l'étude actuelle des systèmes logiques. La polarisation est une contrainte qui simplifie les objets tout en conservant une expressivité suffisante d'un point de vue informatique.<br /><br />L'objet de cette thèse est d'étudier et d'exploiter cette nouvelle structure afin en particulier de mettre à jour les relations entre la logique classique et la logique linéaire (LL). L'introduction des polarités dans LL permet de mieux appréhender ce vaste système et de prolonger le développement de différents outils trop complexes en l'absence de cette contrainte. Nous définissons ainsi, pour la logique linéaire polarisée (LLP), des réseaux de preuve intégrant les connecteurs additifs de manière satisfaisante, une sémantique des jeux polarisés qui réconcilie jeux et dualité, une géométrie de l'interaction parallèle et d'autres sémantiques dénotationnelles basées sur des notions connues (espaces de corrélation, catégories de contrôle).<br /><br />Il est important de montrer que malgré cette contrainte, LLP reste un système suffisamment expressif. Pour cela nous étudions en détail les traductions des différents systèmes de logique classique déterministe connus (LC, lambda-mu calcul, ...) aussi bien en appel par nom qu'en appel par valeur. De surcroît, les traductions obtenues pour ces systèmes sont plus simples que celles vers LL.<br /><br />Enfin la souplesse de ces traductions nous permet d'analyser plus finement certaines propriétés de la logique classique tout comme LL permet d'analyser la logique intuitionniste. On peut ainsi étudier un équivalent linéaire des CPS-traductions.

Page generated in 0.1062 seconds