1,721,046 research outputs found
Reactive Web Programming in a Static Typing Context for Rich Multimedias Content Orchestration
No full textLe but de cette thèse est d'apporter de nouvelles possibilités au domaine de la programmation Web, dont les technologies répandues ne capturent pas toutes les problématiques engendrées par les interactions dans une application. Notre solution est un langage, Pendulum, inspiré de la programmation synchrone réactive en Esterel et se présentant comme une extension à OCaml. Il permet de gagner en sûreté et en expressivité en particulier dans la gestion d'interaction multiples. Dans une première partie, nous présentons notre perception de la programmation Web d'aujourd'hui en partant du standard pour aller vers les technologies plus modernes qui tentent de subvenir aux besoins des programmes par d'autres approches, notamment la programmation multitier et les modèles de concurrence en flot de données. Dans une seconde partie, nous introduisons le langage Pendulum et ses constructions, ce qu'il propose comme interopérabilité avec le client Web le différenciant d'autres langages synchrones, et l'interface de programmation qui le connecte avec le langage hôte. Dans les parties trois et quatre, nous présentons la méthode de compilation utilisée, GRC, pour GraphCode, qui produit un graphe de flot de contrôle à partir du programme synchrone source. On revient sur la structure du GRC, les règles permettant de le construire, ainsi que notre méthode d'ordonnancement statique. Nous décrivons ensuite la génération de l'environnement d'exécution d'un programme synchrone dans le programme hôte. Dans une cinquième partie, nous montrons l'intérêt de la programmation synchrone dans le client et en quoi son modèle d'exécution s'adapte naturellement à celui du navigateur Web. Nous montrons qu'il est possible de profiter de cet avantage pour réagir aux évènements plus efficacement sans efforts d'optimisation. Avant de conclure, nous présentons de multiples exemples implémentés en Pendulum pour mettre en avant les qualités d'expressivité et de sûreté de la programmation synchrone sur différentes problématiques impliquant du multimédia et des interactions.The goal of this thesis is to bring new capabilities to Web programming, whose languages, frameworks don't handle all the problematics raised by interactions in a Web application. Our solution is a programming language, Pendulum, taking its roots in synchronous reactive model à la Esterel. It brings safety and expressiveness, especially when handling multiple interactions. In the first chapter, we give our point of view on what is Web programming today, from the standard to the newest frameworks trying to fill programers needs by other approaches, like multitier programming or dataflow programming. In the second chapter, we introduce Pendulum and its instructions, its interface with the host language, and what it brings to both synchronous and Web programming. In the third and fourth chapter, we present the compilation method, GRC a.k.a GraphCode, that produces a control flow graph from the source code. In the first part, we insist mainly on GRC structure, the rules describing its creation and our technic to linearize parallel branches. Then, we describe the how to initialize synchronous execution environment in OCaml. In the fifth chapter, we show why it is a benefit to use synchronous programming in client programming and how its execution model can natively match the Web browser execution model. We use those ideas to show how a synchronous program can be fast to handle events without optimisation attempt. Before we conclude, we detail several examples implemented with our language to show how expressive and safe synchronous programming can be on diverse programs, implying multimedia and interactions
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Security analysis of system code using static typing
No full textLes noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C.Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Analyses statiques de ressources réutilisables pour langages de haut niveau
No full textIl est important pour les programmeuses et programmeurs de maîtriser la quantité de temps, de mémoire, et d'énergie que leurs programmes consomment. Il s'agit non seulement d'un enjeu écologique, mais aussi une question de sûreté : les logiciels peuvent échouer si les ressources dont ils ont besoin n'existent pas en quantité suffisante quand on les exécute. Cette thèse cherche à améliorer la situation des analyseurs statiques de ressources, en proposant un formalisme "neutre" capable de combiner plusieurs analyses et de les réutiliser sur plusieurs langages de programmation. Ce formalisme est basé sur une machine abstraite et son système de type idoine via la correspondance de Curry-Howard. Au niveau des types, ce formalisme incarne le calcul des séquents linéaire intuitionniste, augmenté au second ordre par l'addition de "paramètres", des variables de type de sortes quelconques. Ces paramètres sont manipulés avec le fragment conjonction/implication de la logique classique du premier ordre, avec une signature fournie par l'utilisateur. Au niveau logiciel, ce système correspond à une machine virtuelle Call-by-Push-Value, avec gestion explicite des ressources, et les paramètres représentent des grandeurs caractéristiques des programmes (tailles, nombre de tour de boucle, etc.). Le système de type de cette machine abstraite produit, en plus d'un programme typé, une contrainte du premier ordre sur les paramètres du programme, à la fois les paramètres libres et ceux liés par des quantificateurs. Cette contrainte étant exprimée dans un fragment de la logique du premier ordre, il est possible de tester sa validité ou sa satisfaisabilité avec un solveur SMT. De plus, dans le cas de paramètres dans signature (int,0,1,+,-,*), il est possible d'éliminer les quantificateurs sans réduire le pouvoir de prédiction dans les cas réalistes. La contrainte résultante peut alors servir de base pour un programme d'optimisation sur les entiers fournissant des bornes sous formes closes de paramètres. Cela permet de fournir des bornes de ressources pour les programmes décrits dans le langage de la machine. La machine abstraite que nous présentons admet de plus un système d'effet de bord permettant d'encoder le passage de ressource dans les programme sans besoin de primitives supplémentaires. Cela facilite la compilation de langages sources dans la machine : un schéma de compilation sans ressources engendre automatiquement un schéma avec ressources, tout en respectant la sémantique opérationnelle du langage source telle que décrite par le premier schéma. Nous démontrons la validité de cette approche via une implémentation "AutoBill". Celle-ci peut prendre en entrée des programmes écrit dans un langage à la ML avec sémantique en appel par valeur pour en Call-by-push-value, ou en langage machine. Ces programmes peuvent inclure des paramètres et des signatures arbitraires. AutoBill renvoie alors la contrainte correspondante dans un format de fichier standard. Le solveur Z3 peut alors fournir les formes closes voulues. Nous présentons l'extensibilité de notre approche en ajoutant des effets de bord monadiques au langage à la ML, et en encodant l'analyse de complexité AARA dans les programmes. Dans ce dernier cas, AutoBill supporte les annotations de tailles et complexités, ce que les implémentations précédentes d'AARA ne supportaient pas.Programmers care about the amount of time, memory, and energy their program require to run. This is not only a matter of ecological ethic, but also of safety: software can fail or degrade in quality when not enough resources are available. This work aims to improve static resource analyzers by proposing a neutral formalism capable of combining several analysis techniques and of reusing them of different languages. This formalism is based on an abstract machine and corresponding type system through the Curry-Howard correspondence. At type-level, it embeds the intuitionistic linear sequent calculus together with "parameters" at the second order. Those parameters are manipulated with the conjunctive-implicative fragment of classical first-order logic, with a user-provided signature. At term level, this corresponds to a call-by-push-value virtual machine, with explicit resource manipulation. Parameters then represent characteristic quantities of data structures and computations (sizes, iteration counts, etc.)Our type system inference generates, together with a typed program, a first-order constraint over the parameters used in said program. Those include both the free parameter variables, but also those bounds by quantifiers. This constraint being first-order, it is amendable to SMT solving. Furthermore, in the important case of integers with signature (int, 0, 1, +, -, *), those quantifiers can be eliminated without significant loss of predictive power in cases found in the wild. This quantifier-free constraint can then be turned into an integer optimisation program, giving closed-form bounds on the values of those parameters. This provides resource bounds to programs written in the machine language. Our abstract machine admits a effect system capable of soundly encoding resource-passing without adding new primitives. This facilitates resource analysis for other languages: any compilation scheme to the machine automatically extends to a resource-aware one, which is sound regarding the operational semantics given by the original scheme. We show the feasibility of our method through its implementation, "AutoBill". It takes as input either a ML-style call-by-value language, a Call-by-Push-Value lambda-calculus, or in machine languages. Parameters with arbitrary user-defined sorts are supported. AutoBill then generates the corresponding constraint in a standard format. The Z3 solver can then provide closed-form bounds on those parameters. The extensibility of our method is demonstrated through the addition of a monadic effect system in the ML-language, and through the encoding of AARA analyses. AutoBill supports parameters annotations for user-described size and complexity, which previous AARA implementations didn't support
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
Dispelling the Myths Behind First-author Citation Counts
Full text linkWe conducted a full-scale evaluative citation analysis study of scholars in the XML research field to explore just how different from each other author rankings resulting from different citation counting methods actually are, and to demonstrate the capability of emerging data and tools on the Web in supporting more realistic citation counting methods. Our results contest some common arguments for the continued
use of first-author citation counts in the evaluation of scholars, such as high correlations between author rankings by first-author citation counts and other citation
counting methods, and high costs of using more realistic citation counting methods that are not well-supported by the ISI databases. It is argued that increasingly available digital full text research papers make it possible for citation analysis studies to go beyond what the ISI databases have directly supported and to employ more
sophisticated methods
koamabayili/VECTRON-author-checklist: VECTRON author checklist
No full textWe have done our best to complete the author checklist relating to the use of animals in the hut study. Note that the objective for the hut study was to evaluate the IRS treatment applications for residual efficacy against Anopheles mosquitoes, including the local An. coluzzii mosquito population. Cows were only used to attract mosquitoes into the huts and no tests were carried out directly on the cows. The author checklist is intended for use with studies where experiments are carried out on animals, which is why we have had such difficulty in completing this for the hut study, as many of the questions do not relate to how the cows were used
- …
