Cette thèse montre comment le calcul formel permet la manipulation d'une grande classe de suites et fonctions solutions d'opérateurs linéaires, la classe des fonctions holonomes. Celle-ci contient de nombreuses fonctions spéciales, en une ou plusieurs variables, et de nom- breuses suites de la combinatoire. Un cadre théorique est tout d'abord introduit pour algorith- miser les propriétés de clôture de la classe holonome, pour y permettre un test à zéro et pour unifier les calculs différentiels sur les fonctions et les calculs de récurrences sur les suites. Ces méthodes s'appuient sur des calculs par une extension de la théorie des bases de Gröbner dans un cadre de polynômes non commutatifs, les polynômes de Ore. Deux types d'algorithmes de sommation et d'intégration symboliques définies et indéfinies sont ensuite développés, dont la justification théorique fait appel à la théorie des D-modules holonomes. Les premiers ont recours à une élimination polynomiale non commutative par bases de Gröbner ; les seconds à des algo- rithmes de résolution de systèmes fonctionnels linéaires en leurs solutions fractions rationnelles. Bien plus que la recherche de formes closes, l'objectif est de pouvoir continuer à calculer avec la représentation implicite des objets holonomes même en l'absence de formes explicites. Ce type de calculs permet en particulier la preuve automatique d'identités sommatoires et intégrales. Une implantation de ces algorithmes dans le système de calcul formel Maple a permis de donner la première preuve automatique d'identités jusqu'à présent inaccessibles par le calcul formel.

La dernière décennie, la complexité des technologies embarqués a explosé et les flots de conception industrielle habituels ne suffisent plus pour proposer des produits fiables en respectant les exigences du marché. Ainsi, le développement de nouvelles méthodologies de conception est devenu un besoin impératif. La thèse vise l'amélioration des méthodologies de conception des systèmes embarqués. En proposant une approche de conception par niveaux d’abstraction, la nouvelle approche permet de guider et d’assister les concepteurs dans les étapes de conception, précisément de raffiner les composants de communication. Elle offre des garanties de préservation des propriétés fonctionnelles le long du flot de conception. La méthode proposée permet de raisonner sur les différents niveaux de description d'un système en exploitant des techniques de preuve de propriétés associées aux raffinement formel. / In the last decade, the complexity of embedded systems has exploded and the usual industrial design flows do not suffice any more to propose reliable products while respecting time to market constrain. Thus, developing new design methodologies has become an imperative. The thesis aims at the improvement of the methodologies of conception of the embedded systems. It proposes a method for assisting the process of refinement along the design flow. The proposed approach splits the design flow into multiple-levels, in order to guide the designer in the design process, from the most abstract model down to a synthesizable model. Furthermore, by using formal techniques the method allows to check the preservation of functional correctness along the design flow.

.

Les serveurs Internet sont des logiciels particuliers. Ils doivent répondre aux demandes d'un grand nombre de clients distants, supporter leur évolution et être robustes car ils ne s'arrêtent jamais. Les modèles de concurrence permettent d'entrelacer les traitements d'un grand nombre de clients. Aucun consensus ne se dégage sur un meilleur modèle. Pour s'abstraire du modèle de concurrence, je propose un modèle de développement de serveurs Internet. Les outils de vérification formelle permettent d'accroître la sûreté des logiciels mais il est nécessaire de leur fournir un modèle simple du logiciel. Le modèle de développement que je propose est utilisé pour générer le serveur et son modèle formel. Le décodage d'une requête cliente dépend du modèle de concurrence. Je propose d'utiliser un générateur d'analyseur syntaxique qui s'abstrait de ce problème et automatise le développement du décodage

Au cours de son activité de conception, l'ingénieur manipule de nombreux modèles mathématiques des dispositifs à concevoir, dimensionner et simuler. Aujourd'hui, le concepteur manipule souvent des modèles identiques pour des objectifs différents. Ceci implique une multiplication des modes de représentation et pose des problèmes de gestion de la ressource de modèle au sein de l'entreprise. Les travaux présentés dans cette thèse apportent une réponse possible pour la capitalisation de cette expertise sous un format a-contcxtucl. La capitalisation ne prend de sens que si la donnée capitalisée est exploitable. Ceci impose de définir une orientation au modèle par le choix de variables d'entrées ou sorties, de paramètres. Ces choix permettent ensuite de déterminer automatiquement un scénario de calcul numérique utilisé pour générer un code dédié à l'outil utilisé.

Ce travail part de l'observation d'un résultat de P. Robba établi en 1982 dont l'énoncé est le suivant : si l est un entier p-adique, alors la série (1+T)l à coefficients dans l'anneau des entiers p-adiques, réduite modulo p, est algébrique sur le corps des fractions rationnelles à coefficients dans le corps fini à p éléments si et seulement si l est rationnel. En remarquant que cette série a une expression très proche de celle d'un endomorphisme du groupe multiplicatif sur l'anneau des entiers p-adiques, on généralise ce résultat à une classe de groupes formels de Lubin-Tate dont le logarithme vérifie une certaine condition d'algébricité. Nous interprétons ensuite ce résultat via le foncteur XK de Fontaine et Wintenberger et en tirons des conséquences sur l'indépendance algébrique des automorphismes de corps locaux. Dans la deuxième partie de ce travail, nous établissons l'analogue du théorème de P. Robba dans le cas des modules de Drinfeld de rang 1 définis sur le complété P-adique de l'anneau des polynômes à coefficients dans un corps fini où P est un polynôme irréductible, unitaire et à coefficients dans ce même corps fini.

Ce mémoire présente mes travaux de recherche de 1988 à 2001, travaux effectués d'abord à l'INRIA Rocquencourt au sein du projet Algo (1988 à 1992), puis à l'INRIA Lorraine et au LORIA dans les projets Euréca (1993 à 1997), PolKA (1998 à 2000), et Spaces (2001). Au niveau thématique, on peut distinguer grosso modo trois phases : une première période allant de 1988 à 1992 où j'ai surtout travaillé sur l'analyse d'algorithmes et la génération aléatoire, une seconde période de 1993 à 1997 où je me suis investi dans le calcul formel et les algorithmes sous-jacents, enfin une troisième période depuis 1998 où je me suis intéressé aux problèmes d'arithmétique exacte en précision arbitraire.

<p>Optioner är värdepapper som ger innehavaren rätten, men inte skyldigheten, att sälja eller att köpa den underliggande tillgången inom en given tidsram och till ett givet pris. Vanligen särskiljs det mellan aktieoptioner och indexoptioner. Fokus i uppsatsen ligger på OMXS30 indexoptioner från år 2006. Syftet med uppsatsen är att undersöka om den implicita volatiliteten enligt Black-Scholes formeln bättre predikterar den framtida faktiska volatiliteten än den historiska volatiliteten. I tidigare studier, bland annat i en sammanfattande studie av Figlewski (1997), har resultaten varit tvetydiga. I uppsatsen har jag kunnat konstatera att den implicita och den historiska volatiliteten är relativt jämlika vid prediktering av den faktiska framtida volatiliteten för 2006 års OMXS30 köp- och säljoptioner.</p>

Optioner är värdepapper som ger innehavaren rätten, men inte skyldigheten, att sälja eller att köpa den underliggande tillgången inom en given tidsram och till ett givet pris. Vanligen särskiljs det mellan aktieoptioner och indexoptioner. Fokus i uppsatsen ligger på OMXS30 indexoptioner från år 2006. Syftet med uppsatsen är att undersöka om den implicita volatiliteten enligt Black-Scholes formeln bättre predikterar den framtida faktiska volatiliteten än den historiska volatiliteten. I tidigare studier, bland annat i en sammanfattande studie av Figlewski (1997), har resultaten varit tvetydiga. I uppsatsen har jag kunnat konstatera att den implicita och den historiska volatiliteten är relativt jämlika vid prediktering av den faktiska framtida volatiliteten för 2006 års OMXS30 köp- och säljoptioner.

Dans la littérature, plusieurs recherches parlent du potentiel de l'utilisation de la technologie dans l'apprentissage de l'algèbre au secondaire. Cependant, peu de ces recherches portent sur la factorisation. Mon travail de recherche a été motivé par ces deux faits et avait pour objectif d'explorer si la calculatrice symbolique pouvait jouer un rôle significatif dans l'apprentissage de la factorisation. Dans ma recherche, je me suis inspirée de l'approche technique/théorique développée par Chevallard (1999), et adaptée ensuite par Artigue (2002a) et Lagrange (2000). Dans cette approche, les composantes technique et théorique sont étroitement liées et la dimension théorique ne peut progresser, dans les environnements technologiques, sans la présence de la dimension technique. Mon but a donc été d'explorer le rôle d'une approche technique/théorique, intégrée dans un environnement où l'on utilise la calculatrice symbolique, pour l'apprentissage de la notion de factorisation chez des élèves en 4ième secondaire. Pour atteindre ce but, j'ai fait une étude comparative entre deux groupes d'élèves de 4ième secondaire ayant des difficultés en algèbre: un groupe dont les élèves avaient chacun accès à une calculatrice symbolique (6 élèves) et un groupe où tel n'était pas le cas (10 élèves). Des feuilles d'activités avec des questions similaires pour les deux groupes ont été réalisées. Avant d'accomplir la séquence didactique composée des activités, les élèves avaient fait un pré-test pour que je puisse voir si les deux groupes avaient des connaissances semblables dans les composantes technique et théorique. La séquence didactique a été suivie par un post-test pour explorer les acquis des élèves et les différences entre les deux groupes. Des notes ont été consignées dans un journal de bord pour chacun des cours avec les deux groupes. De plus, j'ai été l'enseignante des deux groupes lors de cette étude. En comparant les résultats au pré-test des deux groupes, on s'est aperçu qu'ils étaient similaires pour la dimension technique, mais qu'iIs étaient légèrement plus forts pour la dimension théorique dans un groupe. Cependant, les résultats pour la dimension théorique étaient très bas dans les deux groupes. Les résultats au post-test nous ont indiqué que le groupe avec la calculatrice symbolique a accompli plus d'améliorations que le groupe sans calculatrice et ce, dans les deux dimensions (technique et théorique). À la suite de l'analyse des notes gardées dans le journal de bord et des réponses contenues dans les feuilles d'activités des élèves des deux groupes, on a pu dégager trois fonctions remplies par la calculatrice symbolique, qui expliqueraient les améliorations chez les élèves du groupe avec celle-ci. Les trois fonctions jouées par la calculatrice étaient les suivantes: la fonction génératrice de formes exactes, la fonction vérificatrice et la fonction instigatrice de discussions. Cette recherche m'a permis de réaliser que le fait d'avoir rendu accessible une calculatrice à des élèves ayant des difficultés en factorisation a eu un apport positif. En fait, ces jeunes ont plus appris avec cet outil, tant au niveau technique que théorique, que les autres élèves qui n'ont pas eu accès à cet outil. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Factorisation, Calculatrice symbolique, Système de calcul formel, Technique, Théorie, Théorique, Vérificatrice, Génératrice de formes exactes, Instigatrice de discussions.