• 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.
11

Du typage vectoriel / On vectorial typing

Diaz Caro, Alejandro 23 September 2011 (has links)
L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte. / The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.
12

Preuves, types et sous-types

Ruyer, Frédéric 30 November 2006 (has links) (PDF)
Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.
13

Vers un assistant à la preuve en langue naturelle

Patrick, Thévenon 05 December 2006 (has links) (PDF)
Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle.<br><br>L'architecture générale du système se décrit en 4 phases :<br>- analyse de la démonstration par des outils linguistiques ;<br>- traduction de la démonstration dans un langage restreint ;<br>- interprétation du texte traduit en un arbre de règles de déduction ;<br>- validation des règles de déduction à l'aide d'un démonstrateur automatique.<br><br>Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens.<br><br>Cette thèse présente plus en détail ce projet et développe principalement les points suivants :<br>- définition du langage restreint et de son interprétation ;<br>- propriétés du type principal de termes d'un lambda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ;<br>- description du démonstrateur automatique.
14

La notion d'indéfini en lambda calcul

Bertini, Yves 01 July 2005 (has links) (PDF)
La facilité compte parmi les notions les plus fines de l'indéfini en lambda-calcul. Un terme est dit facile s'il peut être identifié à tout autre terme clos arbitraire sans soulever de contradiction. Introduite en 1975 par Jacopini, elle fait depuis l'objet de recherches qui visent à caractériser la forme des termes faciles. Aujourd'hui, de tous les travaux entrepris il se dégage qu'un tel terme doit posséder une périodicité. Être périodique, c'est être équivalent à un sous-terme propre de l'un de ses réduits. Ici, la périodicité apparaîtra sous les traits de l'auto-similarité. Sont auto-similaires les termes dont l'arbre de Berarducci réapparaît comme sous-arbre propre à lui-même. La facilité de tels termes demeure un mystère. À ce jour, nous n'en connaissons que peu d'exemples. Le terme "Y omega_3" constitue un exemple typique dont la question de la facilité reste ouverte. Dans cette thèse, nous étendrons la connaissance de l'ensemble des termes m identiables à Y Omega_3. Nous montrerons que dans un cas critique où lambda-beta +{Y Omega_3 = m} implique m = delta_3, sous certaines hypothèses, m est lui-même auto-similaire. Ils s'en suit une description possible de toutes les équations dérivées de {Y Omega_3= m} sous la forme de classes confinantes.
15

Réalisabilité Classique et protocoles réseaux

Hesse, Philippe 17 July 2008 (has links) (PDF)
Cette thèse étudie différents aspects de la réalisabilité classique due à Jean-Louis Krivine. Celle-ci permet de mettre en oeuvre l'isomorphisme de Curry-Howard: on peut ainsi associer un programme à chaque démonstration mathématique, et considérer chaque théorème comme une spécification. Dans un premier temps, on rappelle le formalisme de la réalisabilité classique ainsi que certains de ses résultats fondamentaux. On s'attache ensuite à l'analyse des contenus opérationnels obtenus suivant deux méthodes différentes d'étude des entiers des modèles de la réalisabilité. Dans un second temps, on rappelle la notion de jeu qui peut être associée à chaque formule du premier ordre dans ce cadre. Ces jeux permettent d'établir une correspondance entre les formules valides du calcul des prédicats et les protocoles de la couche transport des réseaux, que l'on peut spécifier de manière claire et précise par ce biais. La dernière partie est consacrée à l'étude de l'axiome du choix dépendant. On montre que la méthode développée pour le réaliser s'adapte à une expression simple de celui-ci au niveau des individus d'un modèle. On utilise enfin l'instruction associée pour réaliser un cas particulier du théorème de Herbrand. Le terme obtenu effectue une opération très générale, qui peut être interprétée dans le cadre des protocoles réseaux.
16

Typage et déduction dans le calcul de réécriture

Wack, Benjamin 07 October 2005 (has links) (PDF)
Le calcul de réécriture est un lambda-calcul avec filtrage. Cette thèse est consacrée à l'étude de systèmes de types pour ce calcul et à son utilisation dans le domaine de la déduction.<br /><br />Nous étudions deux paradigmes de typage. Le premier est inspiré du lambda-calcul simplement typé, mais un terme peut y être typé sans être terminant. Nous l'utilisons donc pour représenter des programmes et des systèmes de réécriture. La seconde famille de systèmes de types que nous étudions est adaptée des Pure Type Systems. Nous en démontrons la normalisation forte grâce à une traduction vers le lambda-calcul typé.<br /><br />Enfin nous proposons deux approches pour l'utilisation du calcul de réécriture en logique. La première consiste à définir des termes de preuve pour la déduction modulo à l'aide des systèmes fortement normalisants. Dans la seconde, nous définissons une généralisation de la déduction naturelle et nous montrons que le filtrage est utile pour représenter les règles de ce système de déduction.
17

Map Theory et Antifondation

Vallée, Thierry 21 December 2001 (has links) (PDF)
Map Theory est une extension équationnelle du lambda-calcul non-typé conçue par Klaus Grue pour être une fondation commune de l'informatique et des mathématiques. Elle permet en particulier une interprétation complète du calcul des prédicats et de ZFC+FA, où ZFC est la théorie de Zermelo-Fraenkel, et FA est l'axiome de bonne fondation usuel. Toutes les notions primitives de la logique du premier ordre et de la théorie des ensembles, valeurs de vérité, connecteurs, quantificateurs, appartenance et égalité, y sont traduites par des termes du lambda-calcul enrichi de quelques constantes. De plus, Map Theory permet de représenter les types de données inductifs et de donner un sens calculatoire immédiat à tous les constructeurs ensemblistes usuels. La version initiale de Map Theory par K. Grue ne considère cependant que les ensembles (ou classes) bien-fondée relativement à la relation d'appartenance. Dans le cadre du renouveau d'intérêt pour l'antifondation induit par les developpements récents de l'informatique théorique, nous montrons dans notre thèse qu'il est possible d'élaborer une version antifondée de Map Theory qui prenne en compte l'existence des objets non-bien-fondés, et qui permette de raisonner sur ces objets par co-induction. Ce nouveau système ouvre la possibilité d'une représentation directe des types de données co-inductifs, et de la modèlisation des phènoménes et processus circulaires. Dans une première partie, nous présenterons l'axiomatisation MTA de ce nouveau système, et nous montrerons que ZFC+AFA, où AFA est l'axiome d'Antifondation de Aczel-Forti-Honsell, y est interprétable syntaxiquement. Dans la deuxième partie, nous montrerons la consistance de MTA relativement à ZFC+SI, où SI est l'axiome exprimant l'existence d'un cardinal fortement inaccessible.
18

Le calcul de réécriture

Cirstea, Horatiu 07 October 2010 (has links) (PDF)
Le manuscrit présente une partie des travaux de recherche que j'ai effectués au cours des dix dernières années. Je me suis focalisé en particulier sur la présentation du calcul de réécriture comme un formalisme théorique permettant de donner la sémantique dynamique et statique de toute une famille de langages basés sur le filtrage, les règles et les stratégies de réécriture. Je présente le calcul de réécriture général ainsi que plusieurs instances et extensions, en mettant l'accent sur l'expressivité et sur les propriétés de ces calculs. Je montre en particulier que l'intégration uniforme des mécanismes de bases de la réécriture et du lambda-calcul permet une définition précise du processus de réécriture sous des stratégies ainsi que des encodages, typés ou non, de différents formalismes similaires. Je présente dans ce manuscrit des systèmes de types développés dans l'optique d'un formalisme théorique pour le typage dans des langages de programmation à base de règles et je ne discute que brièvement les systèmes de types dépendants étudiés dans une perspective logique. Le filtrage et l'application de substitutions obtenues comme résultat sont des opérations réalisées au niveau méta du calcul de réécriture mais une version explicite permet leur manipulation modulaire et efficace au niveau objet du calcul. Cette version explicite du calcul est étendue avec des structure de graphe permettant de représenter explicitement le partage et les cycles. Je propose également un formalisme général permettant d'exprimer différents calculs à motif et une méthodologie qui met en évidence les points clés permettant d'obtenir la confluence de ces calculs.
19

Syntaxe abstraite typée

Zsido, Julianna 21 June 2010 (has links) (PDF)
Afin de spécifier le comportement des langages de programmation, de préciser leurs propriétés et de certifier leurs implémentations, on étudie des modèles formels des langages de programmation. L'étude se divise en l'étude de la syntaxe et en celle de la sémantique. La deuxième est basée sur des modèles formels de la syntaxe. Cette thèse de doctorat se situe dans l'étude de la syntaxe et est consacrée principalement à deux approches à la syntaxe abstraite typée avec liaison de variables. Ces deux approches utilisent le langage de la théorie des catégories. La premièere approche est dans l'esprit de l'approche catégorique aux théories alébriques. La deuxième est basée sur la notion de monade et introduit la notion d'un module sur une monade qui remplacent les foncteurs et leurs algèbres. En outre la deuxième approche est adaptée pour une classe plus large de syntaxes typées où les types dépendent des termes.
20

Propriétés de sécurité dans le lambda-calcul.

Blanc, Tomasz 07 November 2006 (has links) (PDF)
Nous examinons les propriétés de sécurité du lambda-calcul au travers du prisme du lambda-calcul étiqueté. Les étiquettes expriment dynamiquement la dépendance des termes présents vis-à-vis des réductions passées. Nous montrons que le lambda-calcul étiqueté vérifie la propriété d'irréversibilité des contextes: une fois qu'un contexte est intervenu dans une réduction, il disparaît irréversiblement dans la suite de cette réduction. Nous examinons les propriétés fondamentales de variantes du lambda-calcul étiqueté. Pour cela, nous introduisons une preuve élégante du théorème des développements finis dans la cadre du lambda-calcul par valeur étiqueté. Puis nous prouvons que les étiquettes du lambda-calcul faible expriment le partage. Les étiquettes du lam! bda-calcul permettent d'exprimer des politiques de sécurité telles que l'inspection de pile et la Muraille de Chine. Nous définissons la notion de réduction indépendante de deux principaux A et B: une telle réduction peut se décomposer en deux réductions: une réduction qui ignore A et une réduction qui ignore B. Nous prouvons que la Muraille de Chine garantit cette propriété d'indépendance. Les étiquettes du lambda-calcul permettent aussi d'exprimer la propriété d'interférence: il s'agit ici d'identifier les sous-termes d'un terme M qui influencent le résultat de la réduction de M. Dans le lambda-calcul muni de références, en plus de l'interférence fonctionnelle déjà présente dans le lambda-calcul pur, on identifie l'interférence de mémoire due à l'utilisation des référe! nces. Les étiquettes permettent d'identifier les int! ervalles de temps pendant lesquels une référence influence le résultat d'une réduction.

Page generated in 0.037 seconds