Arithmétiques réelles sur FPGA - Virgule fixe, virgule flottante et système logarithmique.

  • By: Jérémie Detrey
  • Number: PhD2007-01
  • Date: January 2007
  • Abstract:  First introduced as interfaces between other integrated circuits, the FPGA (Field-Programmable Gate Array) reconfigurable circuits have seen number of integrated transistors greatly increase over the last twenty years. This increase was followed by the apparition of other application domains, first with rapid prototyping, and more recently in the acceleration of specific computations. The use of FPGAs is now common practice in digital signal processing, in cryptography or in bio-informatics, to name but a few.
    Some of these applications requiring computations over real numbers, many questions arise with the problem of performing those computations: what accuracy should one require? at what cost? for what speed and thoughput performances?
    The work presented in this thesis aims at answering (at least partially) to these questions. For that purpose, we choose to study various systems for representing real numbers : fixed-point, floating-point and logarithmic number system. Several operators are presented for these three number systems, ranging from basic operators (for floating-point and logarithmic number system) to operators for the evaluation of elementary function (for fixed- and floating-point), with the constant objective to explore all the involved trade-offs as thouroughly as possible. This requires developing generic and flexible algorithms which can be easily adapted to the needs of each particular application. It also involves an accurate and also generic error analysis for each operator in order to guarantee their accuracy.
  • Abstract (in french): À l'origine développés pour être utilisés comme de simples interfaces entre divers circuits intégrés, les circuits reconfigurables FPGA (pour Field-Programmable Gate Arrays) ont gagné en capacité d'intégration ces vingt dernières années. Ce phénomène s'est accompagné d'un important élargissement du domaine d'utilisation de ces circuits, tout d'abord dans la direction du prototypage rapide et plus récemment dans l'accélération de calculs spécifiques. On retrouve ainsi les FPGA en traitement du signal, en cryptographie ou encore en bio-informatique, entre autres.
    Certaines de ces applications nécessitant des calculs sur les nombres réels, de nombreuses questions se posent quant à la réalisation de ces calculs : avec quelle précision calculer ? à quel coût ? pour quelles performances ?
    Les travaux présentés dans cette thèse tentent d'apporter des éléments de réponse à ces questions. Nous choisissons d'étudier divers systèmes de représentations de nombres réels : la virgule fixe, la virgule flottante et le système logarithmique. Divers opérateurs sont présentés pour ces trois systèmes, des opérateurs de base (en virgule flottante et système logarithmique) aux opérateurs pour l'évaluation de fonctions élémentaires (en virgule fixe et virgule flottante), avec la motivation commune de couvrir au mieux les divers compromis qui entrent en jeu. Cela demande donc de développer des algorithmes génériques et souples pour être adaptés aux besoins de chaque application. Cela requiert aussi une analyse d'erreur précise et elle aussi générique pour chaque opérateur de manière à garantir leur précision.
  • Keywords:  Real arithmetic, fixed-point, floating-point, logarithmic number system, LNS, hardware operators, elementary functions, FPGA.
  • Keywords (in french):  Arithmétique réelle, virgule fixe, virgule flottante, système logarithmique, LNS, opérateurs matériels, FPGA.
  • Availability: Electronic copy only.
  • Size: 143p
  • Format: Portable Document Format
  • Get it

Systèmes de types purs et substitutions explicites.

  • By: Romain Kervarc
  • Number: PhD2007-02
  • Date: February 2007
  • Abstract:  Type theory is currently considered as a fundamental tool in computer science, since it establishes a link between a calculus on the one hand and a logical system on the other hand, which allows to state various properties. Pure type systems are a very general formalism in terms of which many logical systems may be expressed. This thesis presents the extension of those systems in two frameworks: a calculus with explicit substitutions and a classical sequent calculus, and studies the properties of the obtained systems, especially type correction, derivation reconstruction, subject reduction, and strong normalisation. In the first case, a new typing rule is introduced, inspired by type inference considerations, and also a new proof method, relying on an order upon derivations. In the second case, the notion of well-formedness is more particularly studied, and one also considers perpetual reorganisations of reduction paths.
  • Abstract (in french): La théorie des types est actuellement considérée comme un outil fondamental en informatique, car elle établit un lien entre un calcul d'une part et un système logique d'autre part, ce qui permet d'exprimer des propriétés variées. Les systèmes de types purs sont un formalisme général dans lequel on peut définir un grand nombre de systèmes logiques. Cette thèse présente l'extension de ces systèmes dans deux cadres : un calcul à substitutions explicites et un calcul de séquents classique, et étudie les propriétés des systèmes obtenus, en particulier la correction des types, la reconstruction de dérivations, la réduction du sujet et la normalisation forte. Dans le premier cas, on introduit une nouvelle règle d'inférence de type inspirée de la synthèse de type et une nouvelle technique de démonstration avec un ordre sur les dérivations. Dans le second cas, on étudie en particulier la notion de bonne formation et l'on s'intéresse à des réorganisations perpétuelles de chemin de réduction.
  • Keywords: Logic, type theory, pure type systems, lambda-calculus, explicit substitution, rewriting system, sequent calculus, Curry-Howard-De Bruijn correspondence, type correction, well-formedness, subject reduction, preservation of strong normalisation, strong normalisation, well-founded order, perpetuality.
  • Keywords (in french): Logique, théorie des types, systèmes de types purs, lambda-calcul, substitution explicite, système de récriture, calcul de séquents, correspondance de Curry-Howard-De Bruijn, correction des types, bonne formation, réduction du sujet, préservation de la normalisation forte, normalisation forte, ordre bien fondé, perpétualité.
  • Availability: Electronic copy only.
  • Size: 210p
  • Format: Compressed postscript
  • Get it

Complexité en requêtes et symétries.

  • By: Vincent Nesme
  • Number: PhD2007-03
  • Date: May 2007
  • Abstract: This work is about the study of the query complexy of symmetric problems, in both frameworks of quantum and classical randomized computing. In the quantum case, we show a new application of the so-called "polynomial" lower bound method to the abelian hidden subgroup problems, via the "symmetrization" technique. In the case of randomized computing, under a "transitive symmetry" hypothesis on the considered problems, we give a combinatorial formula allowing us to compute the exact query complexity of the best nonadaptive algorithm. Moreover, we show that under some symmetry conditions, this best nonadaptive algorithm is optimal amongst general algorithms, which gives an expression of the exact query complexity for the corresponding class of problems.
  • Abstract (in french): Ces travaux portent sur l'étude de la complexité en requê tes de problèmes symétriques, dans les cadres du calcul probabiliste classique et du calcul quantique. Il est montré, dans le cas quantique, une application de la méthode de bornes inférieures dite "polynomiale" au calcul de la complexité en requête des problèmes de sous-groupes cachés abél iens, via la technique de "symétrisation". Dans le cas du calcul probabiliste, sous une hypothèse de "symétrie transitive" des problèmes, il est donné une formule combinatoire permettant de calculer la complexité en requêtes exacte du meil leur algorithme non-adaptatif. De plus, il est mis en évidence que sous certaines hypothèses de symétries, ce meilleur algorithme non- adaptatif est optimal même parmi les algorithmes probabilistes plus gén&e acute;raux, ce qui donne pour la classe de problèmes correspondante une expressio n exacte de la complexité en requêtes.
  • Keywords: Quantum computing, query complexity, hidden subgroup, polynomial method, symmetries, automorphisms, black box, lower bounds, adaptivity.
  • Keywords (in french): Calcul quantique, complexité en requêtes, sous-groupe caché, méthode polynomiale, symétries, automorphismes, boîte noire, bornes inférieures, adaptativité.
  • Availability: Electronic copy only.
  • Size: 125p
  • Format: Portable Document Format
  • Get it

Opérateurs arithmétiques matériels pour des applications spécifiques.

  • By: Nicolas Veyrat-Charvillon
  • Number: PhD2007-04
  • Date: June 2007
  • Abstract: L'arithmétique des ordinateurs est une branche de l'informatique qui traite des systèmes de représentation des nombres, des algorithmes arithmétiques et de leurs implantations matérielles ou logicielles. Cette thèse porte sur l'étude et l'implantation matérielle d'opérateurs pour l'évaluation de fonctions pour des applications spécifiques en traitement du signal et des images et en cryptographie. La première partie présente des opérateurs d'évaluation de fonctions basés sur des approximations polynomiales qui demandent peu de matériel. La seconde partie étudie la génération automatique d'opérateurs à base d'additions et décalages (type SRT) pour l'évaluation de certaines fonctions algébriques. Enfin, la dernière partie présente une implantation efficace et compacte des fonctions de hachage cryptographique de la famille SHA-2. Les différents opérateurs proposés dans cette thèse ont tous été validés sur des circuits FPGA.
  • Abstract (in french): Computer arithmetic is a branch of computer science dedicated to number systems, arithmetic algorithms and their hardware and software implementations. This thesis deals with the study and hardware implementation of operators for the evaluation of functions for specific applications in digital signal and image processing and in cryptography. The first part introduces operators for function evaluation that are based on polynomial approximations that require little hardware. The second part studies the automatic generation of shift-and-add operators (SRT-like) for the evaluation of some algebraic functions. The last part presents an effective and compact implementation of the SHA-2 family of cryptographic hash functions. The various operators proposed in this thesis have been validated on FPGA circuits.
  • Keywords: Hardware arithmetic operators for specific applications.
  • Keywords (in french): arithmétique des ordinateurs, FPGA, opérateur matériel, virgule fixe, approximation polynomiale, algorithme addition/décalage, division, opérateur SRT, générateur VHDL, fonction de hachage cryptographique.
  • Availability: Electronic copy only.
  • Size: 134p
  • Format: Portable Document Format
  • Get it

Utilisation et certification de l'arithmétique d'intervalles dans un assistant de preuves.

  • By: Francisco José Cháves Alonso
  • Number: PhD2007-05
  • Date: September 2007
  • Abstract: Nowadays, more and more calculations, including monitoring and control, are done by software. Our goal is to formally prove the correctness of some numerical calculations by using on computers some tools that have long been guaranteed by human beings like interval calculations, and particularly Taylor models calculations. Yet such theoretical tools are totally unknown to formal proof checkers. This thesis presents the construction of a library of Taylor models for PVS proof checker. We have developed addition, subtraction, multiplication by a scalar, multiplication, square, power and square root operations on Taylor models. We have also developed the exponential, sine, arctangent and hyperbolic sine and cosine on Taylor models. We have proven in PVS that the operations and functions defined in our library preserve the containment property. To the best of our knowledge, such formal proofs have never been done for the implementations of Taylor models. We have developed a PVS strategy called containment to prove the containment property of Taylor models built from the operations and functions defined. We have also developed another strategy called taylors to automatically certify inequalities and bound expressions. When a proof checker is used to establish an inequality, it can be necessary to guide the proof checker step by step during the proof. For this reason, users frequently don't do the proof. Then, our work, that simplifies the proof of inequalities and expressions boundaries, is incentive to the use of formal proof checkers. This work can be used to construct Taylor models of expressions, derive more or less accurate bounds for arithmetic expressions, certify inequalities and bound expressions. We show with two applications that our method for verifying expressions in a proof checker allows us to formally prove some expressions that appear in life critical pieces of software.
  • Abstract (in french): De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor. Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor. Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS. Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques. Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.
  • Keywords: Certification of programs, numerical computations, interval arithmetic, Taylor models, formal proof, proof checker, PVS.
  • Keywords (in french): Certification de programmes, calcul numérique, arithmétique d'intervalles, modèles de Taylor, preuve formelle, PVS.
  • Availability: Electronic copy only.
  • Size: 115p
  • Format: Portable Document Format
  • Get it

Estimation et optimisation des performances temporelles et énergétiques pour la conception de logiciels embarqués.

  • By: Nicolas Fournel
  • Number: PhD2007-06
  • Date: November 2007
  • Abstract: Current technology trend allows hardware designers to embed more and more computational power and features. This trend unfortunately comes with an energy consumption growth which battery technology fails to tackle. Hardware adaptations for energy consumption reduction are limited and need a software control. To help software design in order to optimize hardware capabilities of a platform, developers need feed-back about system energy consumption. We propose a methodology allowing a fast and simple characterization of a complete platform. Model calibration is based on real platform physical measures. This allows the model to be easily adaptable to new systems. We also propose a software simulation tool allowing an easy and fast usage of the previous characterization and a fast identification of the most energy hungry part of the software by providing a source code annotation. This back-annotation fairly reports peripherals consumption by taking into account peripherals asynchronous events.
  • Abstract (in french): L'évolution de la technologie permet aux concepteurs d'intégrer dans les systèmes embarqués de plus en plus de puissance de calcul et de fonctionnalités. Cette croissance de puissance s'accompagne malheureusement d'une hausse de l'énergie consommée par l'appareil que la technologie des batteries est incapable de compenser. Les mécanismes matériels mis en place pour contenir cette consommation dans le but de limiter le poids des batteries ne suffisent plus et nécessitent l'intervention du logiciel pour les contrôler. Pour aider la conception du logiciel afin qu'il tire le meilleur avantage d'un point de vue énergétique des capacités de la plateforme matérielle, le développeur doit avoir des retours sur la consommation électrique du système. Nous proposons dans ces travaux, une méthodologie permettant une caractérisation simple et rapide d'un système matériel complet. La calibration de ce modèle utilise des mesures physiques simples sur le matériel pour le rendre facilement adaptable à de nouveaux systèmes. Nous proposons de même un outil de simulation qui permet une exploitation de cette modélisation en remontant des informations de consommation au niveau du code source de l'application analysée, tout en prenant en charge le désynchronisation entre le logiciel et certains événements matériels.
  • Keywords: Embedded systems, energy consumption characterization, software optimisation, development tools, software simulation.
  • Keywords (in french): Système embarqués, modélisation de la consommation énergétique, optimisation logiciel, outils de développement, simulation logicielle.
  • Availability: Electronic copy only.
  • Size: 137p
  • Format: Portable Document Format
  • Get it

Problèmes de décision et d'évaluation en complexité algébrique.

  • By: Sylvain PERIFEL
  • Number: PhD2007-07
  • Date: December 2007
  • Abstract: In this thesis we are essentially interested in questions concerning algebraic complexity classes of decision problems and of evaluation problems. More precisely, we study on the one hand the model of Blum, Shub and Smale (BSS) for the recognition of languages over arbitrary structures thanks to algebraic circuits, and on the other hand the model of Valiant for the computation of polynomials thanks to arithmetic circuits. Our results show that in order to separate complexity classes, it is easier to work on evaluation problems, that is, in Valiant's model. This confirms our intuition that, the model being simpler (there are no test gates), lower bounds should be easier to obtain. In particular, we show two transfer results. The first concerns the algebraic versions of P and NP: over a field of characteristic zero, the separation of P and NP in BSS model thanks to problems in NP "without multiplication" implies the separation of P and NP in Valiant's model. The second concerns the question "P=PSPACE?": after defining analogues of PSPACE in both algebraic models, we show that separating P and PSPACE, over the reals or over the complex field, is easier in Valiant's model. More succinctly, we also study the manipulation by Turing machines of polynomials given by arithmetic circuits. Indeed, this way of encoding polynomials can be much shorter than the list of monomials. But the study of two examples (computing the coefficient of a monomial and computing the degree of a polynomial) shows that the manipulation of polynomials given by circuits is hard, even if their degree is polynomial and if we work over a field of positive characteristic.
  • Abstract (in french): Dans cette thèse, on s'intéresse essentiellement à des questions concernant les classes de complexité algébrique de problèmes de décision et de problèmes d'évaluation. Plus précisément, nous étudions d'une part, le modèle de Blum, Shub et Smale (BSS) pour reconnaître des langages sur une structure quelconque grâce à des circuits algébriques, et d'autre part, le modèle de Valiant pour calculer des polynômes grâce à des circuits arithmétiques. Nos résultats montrent qu'afin de séparer des classes de complexité, il est moins difficile de travailler sur les problèmes d'évaluation, c'est-à-dire dans le modèle de Valiant. Cela confirme notre intuition que, le modèle étant plus simple (il n'y a pas de portes de tests), les résultats doivent être plus simples à obtenir. En particulier, nous montrons deux résultats de transfert. Le premier concerne les versions algébriques de P et NP : sur un corps de caractéristique nulle, séparer P et NP dans le modèle BSS grâce à des problèmes NP "sans multiplication" implique de séparer P et NP dans le modèle de Valiant. Le second concerne la question "P=PSPACE ?" : après avoir défini un analogue de PSPACE dans les deux modèles algébriques, nous montrons que séparer P de PSPACE, sur les réels ou sur les complexes, est moins difficile dans le modèle de Valiant. Par ailleurs, et plus brièvement, nous étudions également la manipulation par machines de Turing de polynômes donnés par des circuits arithmétiques. En effet, encoder des polynômes de cette façon peut être bien plus court que la liste de tous les monômes. Mais l'étude de deux exemples (calculer le coefficient d'un monôme et calculer le degré d'un polynôme) montre qu'il semble difficile de manipuler des polynômes donnés de cette façon, même lorsqu'ils sont de degré polynomial et que l'on travaille sur un corps de caractéristique non nulle.
  • Keywords: Algebraic complexity, polynomials, algebraic circuits, arithmetic circuits, evaluation problems, decision problems, Boolean complexity.
  • Keywords (in french): Complexité algébrique, polynômes, circuits algébriques, circuits arithmétiques, problèmes d'évaluation, problèmes de décision, complexité booléenne.
  • Availability: Not available.
  • Size: 124p
  • Format: Portable Document Format
  • Get it

Graphes et hypergraphes : complexités algorithmique et algébrique.

  • By: Laurent Lyaudet
  • Number: PhD2007-08
  • Date: December 2007
  • Abstract: The work done during this thesis comes within the scope of hierarchical graph decomposition, and algorithmic and algebraic complexity. The study of branchwidth lead us to look at a problem of hypergraph partitioning. This problem is parameterized by two integers k and l where k is the total number of colors and l is the maximum number of colors a hyperedge is allowed to see. This problem shows surprising variations of complexity. Indeed, for k and l fixed, it is: NP-complete when l>1 and polynomial when l=1 on hypergraphs; NP-complete when l=1 and linear when l>1 on hypergraphs with disjoint hyperedges. This inversion of complexity is partly explained by the weak NP-completeness of the problem when l=1 and the variation in the size of an instance. We also studied the links between hierarchical decompositions and algebraic complexity in collaboration with Uffe Flarup and Pascal Koiran. More precisely, we are interested in classes of complexity from Valiant's model. In this framework, we express polynomials with weighted graph covers such as directed cycle covers, hamiltonian circuits, or perfect matchings. All these covers are related to the permanent and hamiltonian polynomials that are both VNP-complete in Valiant's model (VNP is an algebraic analog to NP). Our work gave us a characterization of the complexity of families of polynomials generated by these covers on particular graph classes. We show notably that on graphs with bounded pathwidth or treewidth the generated polynomials are in fact the whole class of arithmetic formulas. Other results linking classes of graphs and classes of complexity have been obtained.
  • Abstract (in french): Les travaux effectués pendant cette thèse s'inscrivent dans le cadre des décompositions hiérarchiques de graphes et des complexités algorithmique et algébrique. L'étude de la largeur de branche de graphes nous a conduit à étudier un problème de partitionnement d'hypergraphes. La variante de partitionnement d'hypergraphes en question est paramétrée par deux entiers k et l où k est le nombre total de couleurs et l le nombre maximum de couleurs qu'une hyperarête est autorisée à voir. Ce problème présente des variations de complexité surprenantes puisqu'il est, pour l et k fixés, NP-complet quand l>1 et polynomial quand l=1, sur les hypergraphes ; NP-complet quand l=1 et linéaire quand l>1, sur les hypergraphes avec hyperarêtes disjointes. Cette inversion de complexité s'explique en partie par la NP-complétude faible du problème quand l=1 et la variation dans la taille d'une instance. Nous avons aussi étudié les liens entre décompositions hiérarchiques et complexité algébrique en collaboration avec Uffe Flarup et Pascal Koiran. Plus précisément, nous nous intéressons aux classes de complexité du modèle de Valiant. Dans ce cadre, nous exprimons des polynômes avec des couvertures de graphes pondérés, telles que les couvertures par circuits disjoints, par circuit hamiltonien ou les couplages parfaits qui sont liées au permanent et à l'hamiltonien qui sont tous deux VNP-complets dans le modèle de Valiant (VNP est une analogue algébrique de NP). Nos travaux ont permis de caractériser la complexité des familles de polynômes engendrées par ces couvertures sur certaines classes de graphes. Nous avons notamment montré que sur les graphes de largeur linéaire ou arborescente bornée, les familles de polynômes engendrées sont égales aux formules arithmétiques. D'autres résultats liant des classes de graphes et de complexité ont été obtenus.
  • Keywords: Graph decompositions, treewidth, pathwidth, cliquewidth, branchwidth, permanent, hamiltonian, perfect matchings, algebraic complexity, Valiant's model, hypergraph partitioning, FPT, transportation problem.
  • Keywords (in french): Décompositions de graphes, largeur arborescente, largeur linéaire, largeur de clique, largeur de branche, permanent, hamiltonien, couplages parfaits, complexité algébrique, modèle de Valiant, partitionnement d'hypergraphes, FPT, problème de transport.
  • Availability: Electronic copy only.
  • Size: 147p
  • Format: Portable Document Format
  • Get it

Gestion dynamique des tâches dans une architecture micro-éléctronique intégrée, à des fins de basse consommation.

  • By: Philippe Grosse
  • Number: PhD2007-09
  • Date: December 2007
  • Abstract:
    Whereas computing power of DSP or general purpose processors was sufficient for 3G baseband telecommunication algorithms, stringent timing constraints of 4G wireless telecommunication systems require powerful data driven architectures. Managing the complexity of these systems within the energy constraints of a mobile terminal becomes a major challenge for the designers. System level low-power policies have been widely explored for generic software-based systems, but data flow architectures used for high data rate telecommunication systems need specific power management techniques. In this thesis we propose an innovative power optimization scheme tailored to data-flow, self synchronized system. We first present an innovative simulation environment based on gate power analysis and high level modeling realized with PTOLEMY. These tools allow us to target the optimal power management method in our specific context. Then we expose several analytical models and power optimization algorithms which compute the parameters of an optimal DVS policy tailored to our base band modem FAUST. We conclude by a case study, which proves the validity of our approaches on future silicon technologies.
  • Abstract (in french):
    Alors que la puissance de calcul des DSPs ou des architectures centrées “processeur” était suffisante pour les applications de télécommunication 3G, les contraintes temps réel et la complexité des algorithmes sans fil 4G requièrent de puissantes architectures de traitement intensif. Implémenter des systèmes aussi complexes dans les contraintes énergétiques d’un terminal mobile devient un réel enjeu pour les concepteurs de circuits. Si les techniques de gestion “haut niveau” de la consommation ont été largement explorées pour les architectures de traitement logiciel, les circuits de type “flot de données” nécessitent la mise en oeuvre de nouvelles méthodes de gestion de la consommation. Ces travaux de thèse ont permis de définir une méthodologie complète d’optimisation de la consommation adaptée aux architectures “flot de données” auto-synchronisées. Nous présentons tout d’abord un environnement de simulation basé sur des analyses niveau “portes” et une modélisation “haut niveau” réalisé à l’aide du logiciel PTOLEMY. Cet outil d’exploration nous a permis de qualifier les méthodes systèmes de gestion de la consommation dans notre contexte architectural et applicatif. Ensuite, nous exposons plusieurs techniques de modélisation analytique et d’algorithmes d’optimisation permettant de calculer les paramètres d’un DVS optimal pour l’architecture de modem bande de base FAUST. Enfin, la validité de nos approches a été démontrée par une étude de cas effectuée sur plusieurs scénarios de transmission en suivant plusieurs hypothèses “technologiques” différentes.
  • Availability: Electronic copy only.
  • Size: 154p
  • Format: Portable Document Format
  • Get it

Computing with sequents and diagrams in classical logic - calculi *X, dX and ©X.

  • By: Dragisa Zunic
  • Number: PhD2007-10
  • Date: December 2007
  • Abstract:
    This Ph.D. thesis addresses the problem of giving computational interpretation to proofs in classical logic. As such, it presents three calculi reflecting different approaches in the study of this area.
    The thesis consists of three parts.
    The first part introduces the *X calculus, whose terms represent proofs in the classical sequent calculus, and whose reduction rules capture most of the features of cut-elimination in sequent calculus. This calculus introduces terms which enable explicit implementation of erasure and duplication and to the best of our knowledge it is the first such calculus for classical logic.
    The second part studies the possibility to represent classical computation diagrammatically. We present the dX calculus, the diagrammatic calculus for classical logic, whose diagrams originate from *X-terms. The principal difference lies in the fact that dX has a higher level of abstraction, capturing the essence of sequent calculus proofs, as well as the essence of classical cut-elimination.
    The third part relates the first two. It presents the ©X calculus, a one-dimensional counterpart of the diagrammatic calculus. We start from *X, where we explicitly identify terms which should be considered the same. These are the terms that code sequent proofs which are equivalent up to permutations of independent inference rules. They also have the same diagrammatic representation. Such identification induces the congruence relation on terms. The reduction relation is defined modulo congruence rules, and reduction rules correspond to those of dX calculus.
  • Abstract (in french):
    Cette thèse de doctorat étudie l'interprétation calculatoire des preuves de la logique classique. Elle présente trois calculs reflétant trois approches différentes de la question.
    Cette thèse est donc composée de trois parties.
    La première partie introduit le *X calcul, dont les termes représentent des preuves dans le calcul des séquents classique. Les règles de réduction du *X calcul capture la plupart des caractéristiques de l'élimination des coupures du calcul des séquents. Ce calcul introduit des termes permettant une implémentation implicite de l'effacement et de la duplication. Pour autant que nous sachions, c'est le premier tel calcul pour la logique classique.
    La deuxième partie étudie la possibilité de représenter les calculs classiques au moyen de diagrammes. Nous présentons le dX calcul, qui est le calcul diagrammatique de la logique classique, et dont les diagrammes sont issus des *X-termes. La différence principale réside dans le fait que dX fonctionne à un niveau supérieur d'abstraction. Il capture l'essence des preuves du calcul des séquents ainsi que l'essence de l'élimination classique des coupures.
    La troisième partie relie les deux premières. Elle présente le $copy;X calcul qui est une version unidimensionnelle du calcul par diagramme. Nous commencons par le *X, où nous identifions explicitement les termes qui doivent l'être. Ceux-ci sont les termes qui encodent les preuves des séquents qui sont équivalentes modulo permutation de règles d'inférence indépendantes. Ces termes ont également la même représentation par diagramme. Une telle identification induit une relation de congruence sur les termes. La relation de réduction est définie modulo la congruence, et les règles de réduction correspondent à celle du dX calcul.
  • Keywords:
    Classical logic, proofs as programs, Curry-Howard correspondence, X calculus, diagrammatic calculus, sequent calculus, non-determinism.
  • Keywords (in french):
    Logique classique, preuves comme programmes, correspondence de Curry-Howard, calcul X, calcul diagrammatique, calcul des sequents, non-determinisme.
  • Availability: Electronic copy only.
  • Size: 190p
  • Format: Portable Document Format
  • Get it