Global ETD Search

101	Contributions à la vérification formelle d'algorithmes arithmétiques Martin-Dorel, Erik 26 September 2012 (has links) (PDF) 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. [INFO:INFO_OH] Computer Science/Other Arithmétique à virgule flottante Standard IEEE 754 Arrondi correct Dilemme du fabricant de tables Algorithme SLZ Technique de Coppersmith Preuves formelles Coq SSReflect Lemme de Hensel Certificats Racines entières Approximation polynomiale rigoureuse Modèles de Taylor Arithmétique par intervalles Reste de Taylor-Lagrange Fonctions D-finies Racine carrée Norme 2D Midpoints TwoMultFMA Fast2Sum TwoSum Double-arrondi Bibliothèque Flocq
102	Logique linéaire et classes de complexité sous-polynomiales Aubert, Clément 26 November 2013 (has links) (PDF) Cette recherche en informatique théorique construit de nouveaux ponts entre logique linéaire et théorie de la complexité. Elle propose deux modèles de machines abstraites qui permettent de capturer de nouvelles classes de complexité avec la logique linéaire, les classes des problèmes efficacement parallélisables (NC et AC) et celle des problèmes solutionnables avec peu d'espace, dans ses versions déterministes et non-déterministes (L et NL). La représentation des preuves de la logique linéaire comme réseaux de preuves est employée pour représenter efficacement le calcul parallèle des circuits booléens, y compris à profondeur constante. La seconde étude s'inspire de la géométrie de l'interaction, une délicate reconstruction de la logique linéaire à l'aide d'opérateurs d'une algèbre de von Neumann. Nous détaillons comment l'interaction d'opérateurs représentant des entiers et d'opérateurs représentant des programmes peut être reconnue nilpotente en espace logarithmique. Nous montrons ensuite comment leur itération représente un calcul effectué par des machines à pointeurs que nous définissons et que nous rattachons à d'autres modèles plus classiques. Ces deux études permettent de capturer de façon implicite de nouvelles classes de complexité, en dessous du temps polynomial. [INFO:INFO_CC] Informatique/Complexité [MATH:MATH_LO] Mathematics/Logic [MATH:MATH_LO] Mathématiques/Logique Logique Linéaire Complexité Géométrie de l'interaction Algèbre d'opérateur Machines de Turing Alternantes Circuits Booléens Uniformité Réseaux de Preuves
103	L'obligation de coopération dans le statut de Rome : analyse critique du respect des engagements internationaux devant la cour pénale internationale. / The obligation of cooperation in the Status of Rome : analysis criticizes some respect for the international commitments in front of the International Criminal Court Ndiaye, Yaram 27 September 2012 (has links) A l’instar des juridictions qui l’ont précédé dans la répression des crimes internationaux, la Cour pénale internationale a besoin de la coopération des Etats pour exister. C’est une condition d’effectivité de l’action de la Cour qui se traduit par la participation des Etats à la procédure pénale internationale et par l’harmonisation des législations nationales. Toutefois, en dépit de son affirmation dans le Statut, les Etats parties exécutent difficilement l’obligation de coopération. Ces difficultés s’observent tant au niveau de leur participation à la procédure initiée par la Cour que dans l’exercice de la justice au niveau national. De fait, pour un respect des engagements internationaux devant la Cour, l’institution doit surmonter l’obstacle de la souveraineté nationale. Pour atteindre les objectifs fixés, elle doit amener les Etats à dépasser les critères traditionnels de compétence dans le domaine pénal et à taire les résistances souverainistes en la matière. C’est seulement à ce titre qu’elle peut être fonctionnelle, en opposant aux Etats une conception plus étendue de la justice pour laquelle ils se sont engagés. / Following the example of the jurisdictions which preceded her in the repression of the international crimes, the International Criminal Court needs the cooperation of States to exist. It is a condition of effectiveness of the action of the Court that is translated by the participation of States in the international criminal procedure and by the harmonization of the national legislations. But in spite of its assertion in the Status, States execute with difficulty the obligation of cooperation. These difficulties observe as long at the level of their participation in the procedure in front of the Court that in the exercise of the justice at the national level. Actually, for a respect for the international commitments in front of the Court, the institution has to surmount the obstacle of the national sovereignty. To reach the fixed objectives, she has to bring States to exceed the traditional criteria of skill in the penal domain and to keep silent about the resistances of states on the subject. It is only as such that she can be functional, by setting to States a more vast conception of the justice for which they made a commitment. Accords de coopération Compétence universelle Complémentarité Conférence de Rome Exécution des peines Légitimité Loi de coopération Mandat d'arrêt Remise Preuves Souveraineté nationale Témoins Victimes Agreements of cooperation Universal skill Complementarity Conference of Rome Execution of the punishments Legitimacy Laws of cooperation Arrest warrant Delivery National sovereignty Witnesses Vitims Proofs
104	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. Arithmétique à virgule flottante Standard IEEE 754 Arrondi correct Dilemme du fabricant de tables Algorithme SLZ Technique de Coppersmith Preuves formelles Coq SSReflect Lemme de Hensel Certificats Racines entières Approximation polynomiale rigoureuse Modèles de Taylor Arithmétique par intervalles Reste de Taylor-Lagrange Fonctions D-finies Racine carrée Norme 2D Midpoints TwoMultFMA Fast2Sum TwoSum Double-arrondi Bibliothèque Flocq Floating-point arithmetic IEEE 754 standard Correct rounding Table Maker's Dilemma SLZ algorithm Coppersmith's technique Coq formal proofs SSReflect Hensel's lemma Certificates Integral roots Rigorous polynomial approximation Taylor models Interval arithmetic Taylor-Lagrange remainder D-finite functions Square root 2D norms Midpoints TwoMultFMA Fast2Sum TwoSum Double-rounding Flocq library
105	Dépolitisations d'une épidémie - La lutte internationale contre le sida et les politiques de santé en Tanzanie Hunsmann, Moritz 13 June 2013 (has links) (PDF) Alors que les stratégies de lutte contre le sida en Afrique sub-saharienne mettent en jeu des compromis politiques nationaux fondamentaux, elles sont souvent formulées de manière hétéronome et dans un contexte marqué par la prédominance des bailleurs occidentaux. À partir de l'étude du cas tanzanien, cette thèse analyse différents aspects proprement politiques de la lutte contre le sida, à travers une double perspective : l'étude de l'élaboration des stratégies nationales de prévention et de traitement du VIH et l'analyse critique de leurs fondements biologiques et épidémiologiques. La recherche se fonde sur une enquête de terrain combinant 92 entretiens approfondis avec les principaux acteurs institutionnels au niveau national, et l'observation des processus décisionnels lors de réunions programmatiques. Cette thèse met ainsi en évidence l'attention politique inégale accordée aux différents récits causaux de la propagation du virus, et le rôle de ces histoires causales dans la formulation des politiques de prévention. Elle donne à voir les stratégies de non-décision ou de " contournement du politique " qu'adoptent les acteurs face aux arbitrages difficiles qu'impose la définition de priorités dans un contexte d'insuffisance des ressources. Enfin, à partir d'une analyse des controverses au sujet des effets de la réponse internationale au VIH/sida sur la cohérence des politiques de santé en Tanzanie, la thèse explore les contradictions d'une lutte verticale contre le sida dans un contexte marqué par un système de soins défaillant et une mauvaise santé générale de la population. Elle examine, sur cette base, les conditions d'élaboration d'une critique émancipatrice. VIH/sida sida VIH Tanzanie Afrique dépolitisation épidémie lutte contre le sida Afrique subsaharienne économie politique du sida soins de santé primaires Alma Ata prévention du VIH cofacteurs histoires causales transmission iatrogène politiques fondées sur des preuves aide sanitaire aide internationale aide au développement développement triage non-décision priorisation prévention structurelle programmes verticaux TACAIDS ONUSIDA Fonds mondial OMS Banque mondiale PEPFAR hétéronomie accès universel trithérapie antirétroviraux biopolitique souveraineté politiques de santé santé globale santé mondiale santé internationale système de santé distorsions intégration nutrition et VIH dépendance critique émancipatrice après-développement politique de l'urgence aide au développement critique de l'aide vie nue

Page generated in 0.0384 seconds