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:
.
Abstract (in french):
.
Keywords:
.
Keywords (in french):
.
Availability: Not available.
Size: p
Format:Portable Document Format
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é.
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.
