L'objet de cette thèse est de proposer un codage conjoint source-canal de séquences vidéo pour la transmission sur des canaux sans fil. Le système de codage conjoint source-canal est fondée sur un quantificateur vectoriel structuré et une assignation linéaire d'étiquette qui minimisent simultanément la distorsion canal et la distorsion source. Le quantificateur vectoriel qui est construit à partir de constellations provenant de réseaux de points, lesquels satisfont la propriété de diversité maximale, minimise la distorsion source d'une source gaussienne. La distorsion canal est également minimisée par l'étiquetage linéaire. Nous avons étudié les dépendances entre les coefficients d'ondelettes provenant d'une décomposition t+2D, avec ou sans estimation de mouvement afin d'étendre le schéma du codage conjoint source-canal, développé pour les sources gaussiennes, dans le domaine vidéo où la distribution des coefficients est loin d'être gaussienne. Nous proposons un modèle doublement stochastique afin de capturer ces dépendances et nous l'appliquons à la protection des erreurs pour prédire les coefficients perdus et améliorer ainsi la qualité de vidéo. Dans le cas d'un canal gaussien, nous développons deux systèmes, un avec un étiquetage linéaire non codé et l'autre avec un étiquetage linéaire codé utilisant des codes de Reed-Muller. Nous comparons ces deux schémas de codage avec un schéma non-structuré dont l'étiquetage est adapté au canal et avec un coder vidéo scalable. Dans le cas d'un canal de Rayleigh non-sélectif à évanouissements indépendants le schéma devient robuste lorsque nous utilisons une matrice de rotation avant la transmission sur le canal.

Cette thèse concerne le développement et la mise en œuvre d'un environnement pour le calcul scientifique et la modélisation. L'approche retenue est celle d'une décomposition stratifiée des problèmes, ceci dans un double but: marquer le cheminement progressif des étapes de description, allant de l'énoncé informel vers un langage cible en passant par des langages intermédiaires plus ou moins formalisés ; et, d'obtenir une décomposition structurée, modulaire, pour aller du problème initial vers le programme. Dans le but de vérifier la cohérence des descriptions, des schémas de résolutions, des décompositions, nous associons à tout énoncé des conditions logiques dépendant du langage de description. Pour cela, il nous a paru nécessaire d'étudier les formulations logiques décrites par des systèmes polynômiaux sur les corps finis de la forme Z/pZ. L'étude de ces systèmes nous conduisent à traiter le problème de l'élimination des quantificateurs sur un corps fini, le problème du calcul du résultat sur Z/pZ: des algorithmes sont proposés, ainsi qu'une généralisation de la méthode de Dixon-Biard. Le problème de la déduction est aussi abordé. Ces algorithmes nous permettent de vérifier localement la cohérence d'un énoncé mais aussi d'une décomposition de problème. Ceci rend envisageable une vérification globale. Un éditeur de strates sous Grif est présenté

Les récentes avancées technologiques des microphones de type microsystème électromécanique (MEMS) leurs permettent une utilisation sur une large gamme d’amplitudes sonores. Leur niveau de bruit ayant baissé, il devient possible de capter des sons provenant d’une distance plus lointaine, tandis que l’augmentation de leur pression acoustique maximale leur permet de ne pas saturer dans un environnement très bruyant de type concert ou évènement sportif. Ainsi le système électronique de conversion analogique-numérique connecté au microphone devient l’élément limitant les performances du système d’acquisition acoustique. Un besoin de nouvelles architectures de conversion analogique-numérique ayant une plage dynamique augmentée se fait donc ressentir. Par ailleurs, ces microphones étant de plus en plus utilisés dans des systèmes fonctionnant sur batterie, la contrainte de limitation de la consommation devient importante.Dans la bande de fréquences audio, les convertisseurs analogiques-numériques de type sigma-delta sont les plus aptes à obtenir une grande résolution combinée à une faible consommation. Ils sont divisés en deux grandes familles: ceux à temps discret utilisant principalement des circuits à capacités commutées, et ceux à temps continu utilisant des circuits classiques. Cette thèse se concentre sur l’étude et la conception de chacun des deux types de convertisseurs sigma delta, en insistant sur la faible consommation, le faible coût de production (surface occupée) et la robustesse du circuit, cela en vue d’une production de masse pour équipements portables.La conception d’un convertisseur analogique numérique de type sigma-delta à temps discret a été réalisé, ce dernier atteignant un rapport signal sur bruit de 100 décibels sur une bande de 24kHz, pour une puissance consommée de seulement 480μW. Pour limiter la consommation, de nouveaux amplificateurs à base d’inverseurs sont utilisés, et dont la robustesse contre les variations du procédé de fabrication ou de la température a été améliorée. Les spécifications ont été définies grâce au développement d’un modèle de haut-niveau précis, ce qui permet d’éviter le surdimensionnement tout en atteignant les performances voulues. Enfin, un grand ratio de suréchantillonnage a été choisi afin de réduire l’espace utilisé par les capacités commutées, minimisant le coût de fabrication.Après une étude théorique de l’équivalence entre les modulateurs sigma-delta à temps discret et à temps continu, ainsi que des spécificités propres aux modulateurs à temps continu, une réalisation de ces derniers a été effectuée. Celui-ci atteint un rapport signal sur bruit de 95 décibels sur une bande de fréquence de 24kHz, tout en consommant 142μW. Pour réduire la consommation ainsi que l’espace utilisé, un filtre de boucle du second-ordre a été réalisé avec un seul amplificateur, et le quantificateur fait aussi office d’intégrateur grâce à l’utilisation d’une structure d’oscillateurs contrôlés en tension. Ce quantificateur à base d’oscillateurs est réalisé par des cellules numériques, réduisant la consommation et l’espace utilisé, mais est hautement non-linéaire. Cette non-linéarité a été prise en compte par des choix architecturaux afin de ne pas réduire les performances finales du modulateur. / The recent technological advances in microelectromechanical system (MEMS) microphones allow them to be used on a large sound amplitude range. Due to their lower noise level, it becomes possible to capture sound from a faraway distance, while their increased acoustic overload point gives them the ability to capture sound without saturation in a loud environment like a concert or a sport event. Thus, the electronic analog / digital conversion system connected to the microphone becomes the limiting element of the acoustic acquisition system performance. There is then a need for a new analog / digital conversion architecture which has an increased dynamic range. Furthermore, since more and more of these microphones are used in battery-powered devices, the power consumption limitation constraint becomes of high importance.In the audio frequency band, the sigma-delta analog / digital converters are the ones most able to provide a high dynamic range combined to a limited power consumption. They are split in two families: the discrete-time ones using switched-capacitors circuits and the continuous-time ones using more classical structures. This thesis concentrates on the study and the design of both of these two types of sigma-delta converters, with an emphasis on the low-power consumption, the low production cost (area occupied) and the circuit robustness, in sight of a mass production for portable devices.A discrete-time sigma-delta modulator design has been made, the latter reaching a signal to noise ratio of 100dB on a 24kHz frequency bandwidth, for a power consumption of only 480μW. To limit the power consumption, new inverter-based amplifiers are used, with an improved robustness against the variations of the fabrication process or the temperature. Amplifier specifications are obtained thanks to an accurate high-level model developed, which allows to avoid over-design while ensuring that the wanted performances are reached. Finally, a large oversampling ratio has been used to reduce the switched-capacitors area, lowering the modulator cost.After a theoretical study of the equivalence between discrete-time and continuous-time modulators, and of continuous-time modulators specificities, a design of the latter has been made too. It reaches a signal to noise ratio of 95dB on a 24kHz bandwidth, while consuming 142μW. To reduce the power consumption and the occupied area, a second-order loop filter is implemented using a single amplifier, and the quantizer uses a VCO-based structure that provides inherently an integrating stage. The VCO-based quantizer is made using digital cells, lowering the consumption and area, but is highly non-linear. This non-linearity has been handled by architectural choices to not influence the final modulator performances.

Cette these porte sur differents aspects syntaxiques et semantiques de l'intensification implicite dans une construction du francais non standard du type "Marie est belle qu'on en reste ebahi". Cette construction se caracterise par la presence d'un modificateur propositionnel (la prop-que) jouant le role d'un evaluateur de mesures extremes liees au predicat de la proposition matrice ("belle"). Ce modificateur opere sur des echelles de mesures et delimite la mesure reelle en la mettant en rapport avec la consequence qu'il exprime. Comme ce type d'evaluation correlative definit aussi la construction intensive de consequence (CIC), ou l'intensification est lexicalement realisée par les marqueurs d'intensité "tellement", "si", etc., nous proposons que la construction non standard represente un type implicite de la CIC. La CIC-implicite constitue un nouvel objet d'etude pour la description et la formalisation dans le cadre de la grammaire generative (Chomsky 1993, 1995, 2000). L'objectif principal de cette these est de fournir une description detaillee des comportements de la CIC-implicite, d'identifier les contraintes qui la regissent et de proposer un lien derivationnel entre cette derniere et la CIC-explicite. Une comparaison systematique des proprietes des deux CIC montre que les realisations de la CIC-implicite sont plus restreintes. Les restrictions incluent, entre autres, l'impossibilite de l'enchassement par un verbe factif et l'absence de la force interrogative. Une ligne directe peut etre etablie entre les differentes restrictions en termes de la notion pragmatique d'assertion et de la presence du locuteur. Notre derivation de la CIC-implicite, basee sur l'analyse de la CIC-explicite par association tardive proposee par Bhatt et Pancheva (2004, 2007), formalise la notion d'assertion au niveau de la peripherie gauche avec une projection dediee (Haegeman 2006 ; Speas et Tenny 2003). Cette projection, ainsi que l'association de la prop-que modificatrice, permettent d'interpreter et de legitimer la categorie vide qui realise l'intensification dans la CIC-implicite.

Cette these porte sur differents aspects syntaxiques et semantiques de l'intensification implicite dans une construction du francais non standard du type "Marie est belle qu'on en reste ebahi". Cette construction se caracterise par la presence d'un modificateur propositionnel (la prop-que) jouant le role d'un evaluateur de mesures extremes liees au predicat de la proposition matrice ("belle"). Ce modificateur opere sur des echelles de mesures et delimite la mesure reelle en la mettant en rapport avec la consequence qu'il exprime. Comme ce type d'evaluation correlative definit aussi la construction intensive de consequence (CIC), ou l'intensification est lexicalement realisée par les marqueurs d'intensité "tellement", "si", etc., nous proposons que la construction non standard represente un type implicite de la CIC. La CIC-implicite constitue un nouvel objet d'etude pour la description et la formalisation dans le cadre de la grammaire generative (Chomsky 1993, 1995, 2000). L'objectif principal de cette these est de fournir une description detaillee des comportements de la CIC-implicite, d'identifier les contraintes qui la regissent et de proposer un lien derivationnel entre cette derniere et la CIC-explicite. Une comparaison systematique des proprietes des deux CIC montre que les realisations de la CIC-implicite sont plus restreintes. Les restrictions incluent, entre autres, l'impossibilite de l'enchassement par un verbe factif et l'absence de la force interrogative. Une ligne directe peut etre etablie entre les differentes restrictions en termes de la notion pragmatique d'assertion et de la presence du locuteur. Notre derivation de la CIC-implicite, basee sur l'analyse de la CIC-explicite par association tardive proposee par Bhatt et Pancheva (2004, 2007), formalise la notion d'assertion au niveau de la peripherie gauche avec une projection dediee (Haegeman 2006 ; Speas et Tenny 2003). Cette projection, ainsi que l'association de la prop-que modificatrice, permettent d'interpreter et de legitimer la categorie vide qui realise l'intensification dans la CIC-implicite.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.