• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 77
  • 16
  • 7
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 1
  • 1
  • Tagged with
  • 109
  • 50
  • 21
  • 16
  • 15
  • 13
  • 13
  • 13
  • 12
  • 12
  • 12
  • 12
  • 11
  • 10
  • 10
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
101

Thématique des œuvres plastiques contemporaines et indexation documentaire

Régimbeau, Gérard 12 December 1996 (has links) (PDF)
La recherche documentaire sur les œuvres plastiques du 20e siècle fait souvent intervenir la notion de thème. Qu'est-ce qu'un thème artistique dans l'art contemporain et quels liens entretient-il avec les notions de sujet et de motif ? Quelles méthodes et quels moyens adopter pour répondre aux questions qui y font référence ? Telles sont les questions envisagées dans la thèse dont la perspective n'est pas strictement muséographique, mais concerne plus globalement les documents textuels et iconiques édités à propos des œuvres, qui forment les ressources des centres de documentation et des bibliothèques spécialisés. Une première partie précise la position documentologique du problème, au croisement des sciences de l'information et de l'Histoire de l'art contemporain. Une deuxième partie est consacrée à l'observation, l'analyse et l'évaluation des outils : a) documents primaires (index des ouvrages, catalogues d'expositions et périodiques) ; b) systèmes d'indexation pratiqués dans les documents secondaires (répertoires bibliographiques) ; c) bases de données et banques d'images, pour vérifier quels types de renseignements thématiques on peut recueillir grâce à eux. Devant des résultats insuffisants, la question du thème doit être reprise et explorée dans le champ documentaire. La troisième partie développe arguments théoriques, méthodologiques et propositions pour une indexation des thèmes appliquée aux textes et aux reproductions sur les œuvres contemporaines. Les questions particulières du thème dans les œuvres abstraites et "matériologiques" y sont abordées. La conclusion revient sur les nécessités d'une définition de la thématique dans un cadre interdisciplinaire intéressant l'Iconographie, l'Histoire culturelle et les sciences de l'information.
102

Reconstruire la philosophie à partir de l'Afrique : une utopie postcoloniale

Abadie, Delphine 01 1900 (has links)
No description available.
103

Le centre monumental romain d'Appolonia d'Illyrie : images de synthèse et restitutions archéologiques / Roman monumental center in Apollonia of Illyria : computer-generated images and archaeological restitutions

Follain, Éric 18 February 2012 (has links)
Colonie grecque, Apollonia d’Illyrie (Albanie), a connu à l’époque romaine des phases de construction et d’aménagement importantes. En témoigne le centre monumental qui a fait l’objet de fouilles et de dégagements sous la direction du français Léon Rey au début du XXe siècle. Après la seconde guerre mondiale, les équipes albanaises ont poursuivi les recherches archéologiques et ont réalisé les restaurations et les présentations actuelles. Le centre monumental est organisé autour de deux édifices principaux, l’odéon et le monument des agonothètes. Ces lieux d’assemblée attestent du caractère public de ce secteur de la ville comme le fait un arc de triomphe légèrement postérieur. Des boutiques témoignent d’une fonction commerciale annexe. L’aspect religieux est illustré par un temple ionique, entouré d’un portique, associé à un bâtiment nommé usuellement "prytanée", et par un petit sanctuaire. Enfin, un édifice de plan carré peut être soit une bibliothèque soit un Augusteum. Après l’analyse des vestiges accessibles et de la documentation, une approche des fonctions des différents monuments et les renvois aux éléments comparatifs des hypothèses de restitutions sont proposées puis transposées en images de synthèse. Elles sont ensuite assemblées en une vision globale du centre monumental romain, dans son état du début du IIIe siècle ap. J.-C. Dans l’attente de l’achèvement des recherches sur l’agora, localisée à quelques centaines de mètres, cet ensemble pourrait être un complexe architectural dédié au culte impérial dont l’importance aurait attiré, dans le courant du IIe siècle, le bouleuterion que prudemment on désigne encore comme "monument des agonothètes". / During the Roman period, “Apollonia of Illyria”, a greek settlement in Albania, knew several phases of construction and development. This is demonstrated by the study of the monumental center which was the object of excavations supervised by a French archaeologist Léon Rey at the beginning of the XXth century. After World War II, Albanian teams pursued the researches. They realized the restorations and the current presentations. The monumental center is organized around two main buildings, the Odeon and the “monument of Agonothetes”. These meeting places give evidence of the public character of this part of the city, just like the existence of a triumphal arch built later on. Shops also prove the commercial function of this place. Then, the religious function is illustrated by an ionic temple surrounded by a portico associated with a building named “prytaneum’ and by a small sanctuary. Finally, a square building is either a library or an “augusteum”. After an analysis of the visible vestiges and documentation, a report on the functions of the various monuments and a presentation of the comparative elements, the hypothesis of reconstructions will be proposed and transposed into computer-generated images. They will be assembled in a global vision of the roman monumental center at the beginning of the third century. Researches concerning the agora, localized a few hundred meters further, are not achieved yet but this place could be an architectural complex dedicated to imperial cult. During the second century, its importance could have attracted the bouleuterion that remains, for the moment, named as “monument of Agonothetes”. / Kolonia greke e Apolonisë së Ilirisë, në Shqipëri, ka njohur faza të rëndësishme ndërtimi dhe riorganizimi urban në periudhën romake. Këtë e dëshmon qendra monumentale që ka qenë pikësynimi i gërmimeve dhe zbulimeve të kryera nën drejtimin e francezit Leon Rei, në fillim të shekullit të XX. Pas Luftës së II Botërore, ekipet shqiptare kanë vazhduar nxjerrjen në dritë të saj, si dhe kanë realizuar restaurimet dhe pamjet që shohim sot. Qendra monumentale është organizuar rreth dy godinave kryesore, odeoni dhe monumenti i Agonotetëve. Këto vende mbledhjesh dëshmojnë për karakterin publik të kësaj zone të qytetit, ashtu si dhe një hark triumfi pak më i vonshëm. Dyqanet dëshmojnë për një funksion tregtar aneks. Aspekti religjioz ilustrohet me praninë e një tempulli jonik, të rrethuar me një portik, dhe që lidhet me një godinë të ashtuquajtur prytaneum, si dhe me një faltore e vogël. Së fundmi, një ndërtesë në formë katrore mund të jetë ndoshta një bibliotekë apo augusteum. Në përfundim të studimit të rrënojave të dukshme dhe të dokumentacionit përkatës, parashtrohet trajtimi i funksioneve të monumenteve të ndryshme dhe i elementeve krahasuese të rimëkëmbjes hipotetike të tyre, që më tej transformohen në paraqitjet e informatizuara. Më pas, të gjithë elementët janë bashkuar në një pamje gjithëpërfshirëse të qendrës monumentale romake, ashtu siç paraqitej ajo në fillimin e shek. III të e. sonë. Në pritje të përfundimit të kërkimeve në agora, e cila gjendet vetëm disa qindra metra larg, ky ansambël duket të ketë qenë një kompleks arkitekturor që i kushtohej kultit perandorak, rëndësia e të cilit do të tërhiqte përgjatë shek. II të e. sonë buleterionin, që ende në mënyrë të kujdesshme emërtohet si “monumenti i Agonotetëve”.
104

L’histoire du Cabinet des médailles et antiques de la Bibliothèque nationale (1819-1924) : un Cabinet pour l’érudition à l’âge des musées / The History of the Cabinet des médailles et antiques de la Bibliothèque nationale (1819-1924) : a Cabinet of Scholarly Pursuits in the Museum Age

Bodenstein, Felicity 27 June 2015 (has links)
Le Cabinet des médailles et antiques de la Bibliothèque nationale conserve les « bijoux savants » aux origines du collectionnisme occidental avec son médaillier universel, des pierres gravées et des collections d’antiques d’une diversité étonnante. Si celles-ci proviennent pour les parties les plus anciennes, des collections de la maison royale et de trésors ecclésiastiques, cette thèse ne remonte pas aux origines du département mais s’occupe de son destin à l’âge des musées, entre la Restauration, avec l’arrivée au département en 1819 de Désiré Raoul-Rochette (1789-1854) et la période qui suit la première guerre mondiale jusqu’à la mort d’Ernest Babelon (1854-1924). Elle cherche à comprendre, comment ce « parangon des cabinets d’amateurs de jadis » s’est développé, pris comme il l’était entre une tradition antiquaire aristocratique et les exigences de la modernité, républicaine et spécialiste. Elle aborde les différents aspects de la vie du département à l’intérieur du quadrilatère Richelieu. Tout d’abord, comme le portrait d’un lieu d’histoire d’un point de vue institutionnel et architectural qui permet de comprendre la place accordée historiquement à la culture matérielle au sein de la Bibliothèque nationale. Ensuite l’histoire du développement des collections et puis celle de leur valorisation muséographique et scientifique sont examinées au prisme de l’expansion du domaine de l’archéologie et de l’essor des sciences auxiliaires de l’histoire au XIXe siècle. / The Cabinet des médailles et antiques in the French National Library holds a particular place in the vast constellation of Parisian museums. Home to the so-called « bijoux savants » that founded western collecting culture since the Renaissance, it is at once a universal coin cabinet, one of the worlds foremost collections of cut stones and gems, but also a miscellaneous collection of antiquities representing all periods and places. As described in 1930 by one of its curators, it represents a « parangon of amateur cabinets from another time ». This thesis does not directly deal with its prestigious origins but tells one chapter of its long history, looking at how, from the period of the Restoration onwards (beginning with the direction of Désiré Raoul-Rochette in 1819) until the passing of Ernest Babelon in 1924, this cabinet of antiquarian culture and collections adapted and developed to the modern Republican museum age. The life of the department is first considered as a means of understanding the role of material culture and the place of the museum inside France’s national library in the nineteenth century. It then goes on to consider the development of the collections themselves and their scientific and museological exploitation in light of the rapidly expanding practice of archaeology and highly specialised auxiliary sciences of history.
105

Solving dense linear systems on accelerated multicore architectures / Résoudre des systèmes linéaires denses sur des architectures composées de processeurs multicœurs et d’accélerateurs

Rémy, Adrien 08 July 2015 (has links)
Dans cette thèse de doctorat, nous étudions des algorithmes et des implémentations pour accélérer la résolution de systèmes linéaires denses en utilisant des architectures composées de processeurs multicœurs et d'accélérateurs. Nous nous concentrons sur des méthodes basées sur la factorisation LU. Le développement de notre code s'est fait dans le contexte de la bibliothèque MAGMA. Tout d'abord nous étudions différents solveurs CPU/GPU hybrides basés sur la factorisation LU. Ceux-ci visent à réduire le surcoût de communication dû au pivotage. Le premier est basé sur une stratégie de pivotage dite "communication avoiding" (CALU) alors que le deuxième utilise un préconditionnement aléatoire du système original pour éviter de pivoter (RBT). Nous montrons que ces deux méthodes surpassent le solveur utilisant la factorisation LU avec pivotage partiel quand elles sont utilisées sur des architectures hybrides multicœurs/GPUs. Ensuite nous développons des solveurs utilisant des techniques de randomisation appliquées sur des architectures hybrides utilisant des GPU Nvidia ou des coprocesseurs Intel Xeon Phi. Avec cette méthode, nous pouvons éviter l'important surcoût du pivotage tout en restant stable numériquement dans la plupart des cas. L'architecture hautement parallèle de ces accélérateurs nous permet d'effectuer la randomisation de notre système linéaire à un coût de calcul très faible par rapport à la durée de la factorisation. Finalement, nous étudions l'impact d'accès mémoire non uniformes (NUMA) sur la résolution de systèmes linéaires denses en utilisant un algorithme de factorisation LU. En particulier, nous illustrons comment un placement approprié des processus légers et des données sur une architecture NUMA peut améliorer les performances pour la factorisation du panel et accélérer de manière conséquente la factorisation LU globale. Nous montrons comment ces placements peuvent améliorer les performances quand ils sont appliqués à des solveurs hybrides multicœurs/GPU. / In this PhD thesis, we study algorithms and implementations to accelerate the solution of dense linear systems by using hybrid architectures with multicore processors and accelerators. We focus on methods based on the LU factorization and our code development takes place in the context of the MAGMA library. We study different hybrid CPU/GPU solvers based on the LU factorization which aim at reducing the communication overhead due to pivoting. The first one is based on a communication avoiding strategy of pivoting (CALU) while the second uses a random preconditioning of the original system to avoid pivoting (RBT). We show that both of these methods outperform the solver using LU factorization with partial pivoting when implemented on hybrid multicore/GPUs architectures. We also present new solvers based on randomization for hybrid architectures for Nvidia GPU or Intel Xeon Phi coprocessor. With this method, we can avoid the high cost of pivoting while remaining numerically stable in most cases. The highly parallel architecture of these accelerators allow us to perform the randomization of our linear system at a very low computational cost compared to the time of the factorization. Finally we investigate the impact of non-uniform memory accesses (NUMA) on the solution of dense general linear systems using an LU factorization algorithm. In particular we illustrate how an appropriate placement of the threads and data on a NUMA architecture can improve the performance of the panel factorization and consequently accelerate the global LU factorization. We show how these placements can improve the performance when applied to hybrid multicore/GPU solvers.
106

Image Retrieval in Digital Libraries: A Large Scale Multicollection Experimentation of Machine Learning techniques

Moreux, Jean-Philippe, Chiron, Guillaume 16 October 2017 (has links)
While historically digital heritage libraries were first powered in image mode, they quickly took advantage of OCR technology to index printed collections and consequently improve the scope and performance of the information retrieval services offered to users. But the access to iconographic resources has not progressed in the same way, and the latter remain in the shadows: manual incomplete and heterogeneous indexation, data silos by iconographic genre. Today, however, it would be possible to make better use of these resources, especially by exploiting the enormous volumes of OCR produced during the last two decades, and thus valorize these engravings, drawings, photographs, maps, etc. for their own value but also as an attractive entry point into the collections, supporting discovery and serenpidity from document to document and collection to collection. This article presents an ETL (extract-transform-load) approach to this need, that aims to: Identify and extract iconography wherever it may be found, in image collections but also in printed materials (dailies, magazines, monographies); Transform, harmonize and enrich the image descriptive metadata (in particular with machine learning classification tools); Load it all into a web app dedicated to image retrieval. The approach is pragmatically dual, since it involves leveraging existing digital resources and (virtually) on-the-shelf technologies. / Si historiquement, les bibliothèques numériques patrimoniales furent d’abord alimentées par des images, elles profitèrent rapidement de la technologie OCR pour indexer les collections imprimées afin d’améliorer périmètre et performance du service de recherche d’information offert aux utilisateurs. Mais l’accès aux ressources iconographiques n’a pas connu les mêmes progrès et ces dernières demeurent dans l’ombre : indexation manuelle lacunaire, hétérogène et non viable à grande échelle ; silos documentaires par genre iconographique ; recherche par le contenu (CBIR, content-based image retrieval) encore peu opérationnelle sur les collections patrimoniales. Aujourd’hui, il serait pourtant possible de mieux valoriser ces ressources, en particulier en exploitant les énormes volumes d’OCR produits durant les deux dernières décennies (tant comme descripteur textuel que pour l’identification automatique des illustrations imprimées). Et ainsi mettre en valeur ces gravures, dessins, photographies, cartes, etc. pour leur valeur propre mais aussi comme point d’entrée dans les collections, en favorisant découverte et rebond de document en document, de collection à collection. Cet article décrit une approche ETL (extract-transform-load) appliquée aux images d’une bibliothèque numérique à vocation encyclopédique : identifier et extraire l’iconographie partout où elle se trouve (dans les collections image mais aussi dans les imprimés : presse, revue, monographie) ; transformer, harmoniser et enrichir ses métadonnées descriptives grâce à des techniques d’apprentissage machine – machine learning – pour la classification et l’indexation automatiques ; charger ces données dans une application web dédiée à la recherche iconographique (ou dans d’autres services de la bibliothèque). Approche qualifiée de pragmatique à double titre, puisqu’il s’agit de valoriser des ressources numériques existantes et de mettre à profit des technologies (quasiment) mâtures.
107

Étude de la perception de dirigeants de bibliothèques universitaires québécoises envers un système technologique innovant : les plateformes de services pour bibliothèques

Bertrand, Nicolas 11 1900 (has links)
L’innovation est un sujet d’intérêt en bibliothéconomie. Aussi, ce mémoire de maîtrise explore l'innovation en bibliothèques universitaires en cherchant à comprendre les perceptions de dirigeants de ces bibliothèques sur un outil innovant et sur son adoption potentielle au sein d’un regroupement : les plateformes de services pour bibliothèques (PSB). Ces plateformes sont décrites comme étant mieux intégrées que le système intégré de gestion de bibliothèque. Elles donnent accès à des données bibliographiques partagées et proposent de nouveaux flux de travail. Elles facilitent aussi la mutualisation des ressources entre plusieurs bibliothèques. Dans cette étude de cas simple, des entrevues semi-dirigées ont été réalisées auprès de sept dirigeants du groupe SB9, un réseau de bibliothèques de l’Université du Québec, pour recueillir leurs perceptions sur les PSB, à la suite de l’amorce d’une réflexion en vue d’une adoption partagée. Des résultats ressortent les avantages et les désavantages de ces systèmes pour les bibliothèques universitaires au sein d’un regroupement. Ils permettent aussi d’évaluer la compatibilité de ces systèmes avec leur contexte et la complexité liée à leur adoption. Enfin, ils font ressortir les sources d’influence poussant à l’adoption des PSB. Cette étude met en évidence comment l’adoption potentielle d’une innovation technologique peut agir comme levier pour la transformation organisationnelle, la création de services à valeur ajoutée pour les usagers et de nouvelles collaborations entre bibliothèques. L’impact des PSB va au-delà de leurs fonctionnalités, offrant de nouvelles opportunités aux bibliothèques. Enfin, cette étude offre une perspective nouvelle sur l’innovation dans les bibliothèques universitaires du Québec. / Innovation is a topic of interest in librarianship. Therefore, this master’s thesis aims to explore innovation in academic libraries by examining how library managers perceive an innovative tool, the library services platform (LSP), and its potential adoption by a group of libraries. These platforms are described as being better integrated than integrated library systems. They provide access to shared bibliographic data and allow for new workflows. Moreover, they facilitate resource sharing among several libraries. In this simple case study, semi-structured interviews were conducted with seven library managers from the SB9 group, a network of libraries affiliated with the Université du Québec with the aim of gathering their perceptions of these innovative tools. At the time of data collection, the group was at the stage of considering the shared adoption of an LSP. Results highlight the advantages and disadvantages of such systems for academic libraries in a consortium context. They also shed light on the compatibility of LSPs in context, as well as the complexity associated with their adoption. Finally, they show the sources of influence driving the adoption of LSPs. This study demonstrates how the potential adoption of a technological innovation can act as a lever for organizational change, for the creation of value-added services for patrons, and for new collaborations between libraries. The impact of LSPs goes beyond their mere functionalities, offering new opportunities for libraries. Finally, this study provides a new perspective on innovation in Quebec academic libraries.
108

La Bibliothèque d'Apollodore et les mythographes anciens / Apollodorus’ Library and the ancient Greek mythographers

Contensou, Antoine 22 March 2014 (has links)
La Bibliothèque d’Apollodore, probablement composée au IIe ou au IIIe s. ap. J.-C., vise à rassembler les légendes et les mythes grecs en un système cohérent organisé selon un plan généalogique. Son auteur fonde son travail sur les écrits qui faisaient autorité en la matière, en particulier ceux des grands mythographes en prose du Ve s., parmi lesquels Phérécyde et Acousilaos sont les plus souvent nommés par Apollodore. Ce travail se propose d’analyser les rapports entre ces deux mythographes anciens et la Bibliothèque. Il examine chaque mention de leur nom dans cet ouvrage, et confronte tous leurs fragments au texte de la Bibliothèque, afin de comprendre pourquoi Apollodore choisit de les nommer ou, au contraire, de ne pas le faire ; pourquoi il les suit ou pourquoi il s’en écarte ; quelle place ils occupent réellement dans son traité. Plus largement, ce travail présente une réflexion sur les liens génériques entre la Bibliothèque et les mythographes anciens, en examinant en particulier la question de leur écriture, afin de comprendre comment Apollodore se situe par rapport aux premiers traités mythographiques grecs. / Apollodorus’ Library, probably written during the 2nd or 3rd century A. D., aims at gathering Greek legends and myths in a coherent system based upon a genealogical structure. Its author bases his work on the most authoritative sources, including prestigious 5th-century mythographers as Pherecydes and Acusilaus, whose names are the most mentioned ones in Apollodorus’ treatise, along with Hesiod’s. This work analyses the links between those two ancient mythographers and the Library. It takes a close look at every mention of their name, and compares all their fragments to Apollodorus’ text, in order to understand how and why he cites them or not ; why he draws on them or chooses other sources ; what is their real influence on his treatise. This study also offers a reflection about the links between the Library and the ancient mythographical tradition as a genre, mainly on the basis of their respective style.
109

Contributions à la vérification formelle d'algorithmes arithmétiques / Contributions to the Formal Verification of Arithmetic Algorithms

Martin-Dorel, Erik 26 September 2012 (has links)
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.

Page generated in 0.1182 seconds