Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

La conception des bibliothèques d’évaluation de fonctions est un activité complexe qui requiert beaucoup de soin et d’application, particulièrement lorsque l’on vise des niveaux élevés de fiabilité et de performances. En pratique et de manière habituelle, on ne peut se livrer à ce travail sans disposer d’outils qui guident le concepteur dans le dédale d’un espace de solutions étendu et complexe mais qui lui garantissent également la correction et la quasi-optimalité de sa production. Dans l’état actuel de l’art, il nous faut encore plutôt raisonner en termes de « boite à outils » d’où le concepteur doit tirer et combiner des mécanismes de base, au mieux de ses objectifs, plutôt qu’imaginer que l’on dispose d’un dispositif à même de résoudre automatiquement tous les problèmes.Le présent travail s’attache à la conception et la réalisation de tels outils dans deux domaines:∙ la consolidation du test d’arrondi de Ziv utilisé, jusqu’à présent de manière plus ou moins empirique, dans l’implantation des approximations de fonction ;∙ le développement d’une implantation de l’algorithme SLZ dans le but de résoudre le « Dilemme du fabricant de table » dans le cas de fonctions ayant pour opérandes et pour résultat approché des nombres flottants en quadruple précision (format Binary64 selon la norme IEEE-754). / The design of function evaluation libraries is a complex task that requires a great care and dedication, especially when one wants to satisfy high standards of reliability and performance. In actual practice, it cannot be correctly performed, as a routine operation, without tools that not only help the designer to find his way in a complex and extended solution space but also to guarantee that his solutions are correct and (almost) optimal. As of the present state of the art, one has to think in terms of “toolbox” from which he can smartly mix-and-match the utensils that fit better his goals rather than expect to have at hand a solve-all automatic device.The work presented here is dedicated to the design and implementation of such tools in two realms:∙ the consolidation of Ziv’s rounding test that is used, in a more or less empirical way, for the implementation of functions approximation;∙ the development of an implementation of the SLZ-algorithm in order to solve the Table Maker Dilemma for the function with quad-precision floating point (IEEE-754 Binary128 format) arguments and images.

Le développement exponentiel de la technologie et le vieillissement de la population permettent d’introduire dans notre quotidien les robots d’assistance. La coexistence de l’homme avec ces robots intelligents et autonomes soulève une question fondamentale: dans l’éventualité où un robot provoquerait un accident causant un dommage à une personne ou à un bien qui serait le responsable? Aucune loi ne réglemente les activités de la robotique d’assistance dans le monde. Cette étude vise l’analyse de l’applicabilité des régimes de responsabilité du Code Civil du Québec aux cas de dommages causés par le robot d’assistance. L’analyse des régimes de responsabilité du Code civil du Québec permet de constater que deux régimes de responsabilité sont susceptibles d’être appliqués aux cas spécifiques de dommages causés par le robot d’assistance: le régime de responsabilité du fait des biens, énoncé à l’article 1465 C.c.Q., et le régime de responsabilité du fait des fabricants et vendeurs spécialisés, énoncé à l’article 1468 C.c.Q. Cela s’explique par la présence de critères et de conditions de mise en œuvre des régimes qui sont transposables aux différents aspects concernant la fabrication et l’utilisation du robot d’assistance. / The exponential development of technology and the aging of the population foster the introduction of assistive robots in our daily life. The coexistence of man with these intelligent and autonomous robots raises a fundamental question: in the event that a robot would cause an accident bringing about injury to a person or to property, who would be responsible? No law regulates the activities of assistive robotics in the world. This study aims at analysing the applicability of the Civil Code of Quebec liability regimes to cases of damages caused by assistive robots. The analysis of the liability regimes existing in the Civil Code of Quebec shows that two systems of liability may be applied to the specific cases of damages caused by assistive robots: the regime of liability for property enunciated in Article 1465 of the C.C.Q., and the regime of liability for manufacturers and specialized sellers contained in Article 1468 of the C.C.Q. This is due to the presence of criteria and conditions of implementation of the regimes that are transferable to the different aspects of manufacture and use of assistive robots.

Situé en plein cœur de Paris, le Sentier reconnu depuis la seconde moitié du XXe siècle comme le centre le plus actif du commerce international des tissus, s’est construit dans la continuité d’un ‘’Sentier ancien ‘’ qui trouve ses origines dans la première moitié du XIXe siècle. En nous appuyant sur les Almanachs du Commerce de Paris pour reconstruire l’infrastructure économique de cet espace, nous avons pu mettre en évidence les caractéristiques de cet ensemble originaire et plus particulièrement la croissante centralité du quartier Montmartre dans le commerce des tissus. Placé à la lisière des grands boulevards et des lieux de la « nouvelle modernité » parisienne, ce quartier était le véritable noyau central du commerce des tissus en gros, animé par un négoce important et solidement implanté dans les rues du Sentier, Saint-Fiacre et des Jeûneurs. Il s’agit prioritairement, au début du siècle, du commerce des articles de toiles de coton et des châles, rejoints à partir des années 1830, par la vente de dentelles, de tissus mérinos et de tissus de nouveautés.Dans notre recherche pour saisir l’ensemble des éléments à l’œuvre dans la construction identitaire de cet espace original, l’exploitation de diverses sources, telles que les sources cadastrales, la composition des listes électorales ou les archives notariales, nous ont permis de restituer une image précise de ces dynamiques, de dégager l’importance de cette sphère professionnelle et ses multiples conséquences sur l’espace physique et social de ce quartier. / Located in the very heart of Paris, the SENTIER which prevails in the second half of the 19th century as the most active center of the business of international trade of fabrics, built itself in the continuity of a " former SENTIER " which has its origins in the first half of the 19th century. Relying on the Almanachs of the Trade of Paris to reconstruct the economic infrastructure of this space, we were able to highlight the characteristics of this first socio-economic group and the increasing centrality of the Montmartre neighborhood in the trade of fabrics. Located at the edge of the places of the "new Parisian modernity ", this district became the central point of the wholesale fabrics trade, led by an important trade firmly established in the streets of the Sentier, Saint Fiacre and Jeuneurs. It mainly concerns, at the beginning of the century, the trade of articles of cotton cloths and shawls, joined from 1830s, by the sale of laces, merino fabrics and fashionable fabrics. In our search to seize all the elements in action in the identity construction of this original space, the exploitation of diverse sources, such as the cadastral sources, the composition of electoral rolls or the notarial archives, allowed us to restore a precise image of these dynamics to express the importance of this professional sphere and its multiple consequences on the physical and social space of this district.

Les réseaux euclidiens sont un outil particulièrement puissant dans<br />plusieurs domaines de l'algorithmique, en cryptographie et en théorie<br />algorithmique des nombres par exemple. L'objet du présent mémoire est dual : nous améliorons les algorithmes de réduction des réseaux,<br />et nous développons une nouvelle application dans le domaine<br />de l'arithmétique des ordinateurs. En ce qui concerne l'aspect algorithmique, nous nous intéressons aux cas des petites dimensions (en dimension un, où il s'agit du calcul de pgcd, et aussi en dimensions 2 à 4), ainsi qu'à la description d'une nouvelle variante de l'algorithme LLL, en dimension quelconque. Du point de vue de l'application, nous utilisons la méthode<br />de Coppersmith permettant de trouver les petites racines de polynômes modulaires multivariés, pour calculer les pires cas pour l'arrondi des fonctions mathématiques, quand la fonction, le mode d'arrondi, et la précision sont donnés. Nous adaptons aussi notre technique aux mauvais cas simultanés pour deux fonctions. Ces deux méthodes sont des pré-calculs coûteux, qui une fois <br />effectués permettent d'accélérer les implantations des fonctions mathématiques élémentaires en précision fixée, par exemple en double précision.<br /><br />La plupart des algorithmes décrits dans ce mémoire ont été validés<br />expérimentalement par des implantations, qui sont<br />disponibles à l'url http://www.loria.fr/~stehle.

Responsabilité du fait du produit c’est le nom, donné à un domaine de droit concernant la responsabilité des personnes qui s’occupent à fabriquer et vendre ou distribuer par d’autres moyens des produits pour les différents sorts des dommages causés aux consommateurs et même aux tierces personnes par les défauts de sécurité de ces produits. Cette responsabilité est une responsabilité sans faute qui va au-delà distinction traditionnelle entre la responsabilité contractuelle ou extra-contractuelle. Il existe différents modèles de la responsabilité du fait des produits défectueux dans le monde. Parmi eux le droit américain et le droit européen de la responsabilité du fait des produits sont particulièrement significatifs. Aux Etats-Unis la section 402A de la seconde restatement of torts déterminait le régime de la responsabilité du fait des produits. En 1998 l’institut de droit américain a publié la troisième restatement of torts sous le nom de la responsabilité du fait des produits, ce qui est censé de remplacer la section 402A de la seconde restatement of torts. En Europe, la directive communautaire numéro (85/374/CEE) du conseil du 25 juillet 1985 relative au rapprochement des dispositions législatives, réglementaires et administratives des États membres en matière de responsabilité du fait des produits défectueux constitue le droit spécial des états membres en matière de la responsabilité du fait des produits défectueux. Cette directive a été transposée en droit français par la loi du 19 mai 1998 sous la forme des articles 1386-1 à 1386-18 du code civil français. La faute constitue la seule base légale de la responsabilité civile des vendeurs et des fabricants des produits défectueux en droit iranien. Pour résoudre les conflits de lois et des juridictions qui résultent de l’exportation de produits au niveau international on peut mettre œuvre les conventions et les règlements internationales qui ont été élaborées en la matière ainsi que le droit commun des conflits des lois et des juridictions des pays. / Products liability is the name of a field of law concerning the liability of persons who are engaged in the business of selling or otherwise distributing products who sell or distribute a defective product for harm to persons or property caused by the defect. They are strictly liable. Their liability is a kind of liability which goes beyond the traditional distinction between the contractual and tortious liability. The United-States of America and European Union have the most developed products liability laws in the world. In the United-States the American Law Institute memorialized precedential rule of strict products liability in tort in §402A of the Second Restatement of Torts, and officially promulgated it in 1965. In 1992, the American Law Institute began working on a new Restatement (Third) of Torts on the specific topic of products liability law, approving the new Restatement in 1997 and publishing it in 1998 as The Restatement (Third) of Torts: Products Liability. In Europe, Council Directive of 25 July 1985 on the approximation of the laws, regulations and administrative provisions of the Member States concerning liability for defective products (85/374/EEC) constitutes specific law of products liability of European Union member states. This directive has been transposed in French law by 19 May 1998 act and formed articles 1386-1 to 1386-18 of civil code. Fault is the only legal basis of Iranian products liability law. For solving conflicts of laws and jurisdictions which arise from international trade of products and determining the applicable law and competent jurisdiction we can implement international conventions and regulations which have been elaborated on this subject as well as traditional rules of conflicts of laws and jurisdictions of the countries.

No description available.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le "dilemme du fabricant de tables" (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'"approximation polynomiale rigoureuse", permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre "vérifieur ISValP" est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en "précision augmentée" pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de "double-arrondi", qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis.

De plus en plus de constructeurs proposent des accélérateurs de calculs à base de circuits reconfigurables FPGA, cette technologie présentant bien plus de souplesse que le microprocesseur. Valoriser cette flexibilité dans le domaine de l'accélération de calcul flottant en utilisant les langages de description de circuits classiques (VHDL ou Verilog) reste toutefois très difficile, voire impossible parfois. Cette thèse a contribué au développement du logiciel FloPoCo, qui offre aux utilisateurs familiers avec VHDL un cadre C++ de description d'opérateurs arithmétiques génériques adapté au calcul reconfigurable. Ce cadre distingue explicitement la fonctionnalité combinatoire d'un opérateur, et la problématique de son pipeline pour une précision, une fréquence et un FPGA cible donnés. Afin de pouvoir utiliser FloPoCo pour concevoir des opérateurs haute performance en virgule flottante, il a fallu d'abord concevoir des blocs de bases optimisés. Nous avons d'abord développé des additionneurs pipelinés autour des lignes de propagation de retenue rapides, puis, à l'aide de techniques de pavages, nous avons conçu de gros multiplieurs, possiblement tronqués, utilisant des petits multiplieurs. L'évaluation de fonctions élémentaires en flottant implique souvent l'évaluation en virgule fixe d'une fonction. Nous présentons un opérateur générique de FloPoCo qui prend en entrée l'expression de la fonction à évaluer, avec ses précisions d'entrée et de sortie, et construit un évaluateur polynomial optimisé de cette fonction. Ce bloc de base a permis de développer des opérateurs en virgule flottante pour la racine carrée et l'exponentielle qui améliorent considérablement l'état de l'art. Nous avons aussi travaillé sur des techniques de compilation avancée pour adapter l'exécution d'un code C aux pipelines flexibles de nos opérateurs. FloPoCo a pu ainsi être utilisé pour implanter sur FPGA des applications complètes.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le «dilemme du fabricant de tables» (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'«approximation polynomiale rigoureuse», permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre «vérifieur ISValP» est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en «précision augmentée» pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de «double-arrondi», qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis. / The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the ``Table Maker's Dilemma'' (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of ``Rigorous Polynomial Approximation'', allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel's lemma that we have formalized for both univariate and bivariate cases. In particular, our ``ISValP verifier'' is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of ``augmented-precision'' FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the ``double-rounding'' phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.