bluuebunny/crossref_metadata_2025 huggingface dataset:
The latency, accuracy, and battery (LAB) abstraction
Authors: Kansal Aman , Saponas Scott , Brush A.J. Bernheim , McKinley Kathryn S. , Mytkowicz Todd , Ziola Ryder
Published: November 2013

Emerging mobile applications that sense context are poised to delight and entertain us with timely news and events, health tracking, and social connections. Unfortunately, sensing algorithms quickly drain the phone's battery. Developers can overcome battery drain by carefully optimizing context sensing but that makes programming with context arduous and ties applications to current sensing hardware. These types of applications embody a twist on the classic tension between programmer productivity and performance due to their combination of requirements.

This paper identifies the latency, accuracy, battery (LAB) abstraction to resolve this tension. We implement and evaluate LAB in a system called Senergy. Developers specify their LAB requirements independent of inference algorithms and sensors. Senergy delivers energy efficient context while meeting the requirements and adapts as hardware changes. We demonstrate LAB's expressiveness by using it to implement 22 context sensing algorithms for four types of context (location, driving, walking, and stationary) and six diverse applications. To demonstrate LAB's energy optimizations, we show often an order of magnitude improvements in energy efficiency on applications compared to prior approaches. This relatively simple, priority based API, may serve as a blueprint for future API design in an increasingly complex design space that must tradeoff latency, accuracy, and efficiency to meet application needs and attain portability across evolving, sensor-rich, heterogeneous, and power constrained hardware.
Flexible access control for javascript
Authors: Richards Gregor , Hammer Christian , Zappa Nardelli Francesco , Jagannathan Suresh , Vitek Jan
Published: November 2013

Providing security guarantees for systems built out of untrusted components requires the ability to define and enforce access control policies over untrusted code. In Web 2.0 applications, JavaScript code from different origins is often combined on a single page, leading to well-known vulnerabilities. We present a security infrastructure which allows users and content providers to specify access control policies over subsets of a JavaScript program by leveraging the concept of delimited histories with revocation. We implement our proposal in WebKit and evaluate it with three policies on 50 widely used websites with no changes to their JavaScript code and report performance overheads and violations.
Interacting with dead objects
Authors: Salkeld Robin , Kiczales Gregor
Published: November 2013

Debugging and analyzing a snapshot of a crashed program's memory is far more difficult than working with a live program, because debuggers can no longer execute code to help make sense of the program state. We present an architecture that supports the restricted execution of ordinary code starting from the snapshot, as if the dead objects within it had been restored, but without access to their original external environment. We demonstrate the feasibility of this approach via an implementation for Java that does not require a custom virtual machine, show that it performs competitively with live execution, and use it to diagnose an unresolved memory leak in a mature mainstream application.
Option contracts
Authors: Dimoulas Christos , Findler Robert Bruce , Felleisen Matthias
Published: November 2013

Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious run-time cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails.

In response, we propose
option contracts
as an addition to the contract tool box. Our key insight is that in ordinary contract systems, server components impose their contract on client components, giving them no choice whether to trust the server's promises or check them. With option contracts, server components may choose to tag a contract as an option and clients may choose to exercise the option or accept it, in which case they also shoulder some responsibility. We show that option contracts permit programmers to specify flexible checking policies, that their cost is reasonable, and that they satisfy a complete monitoring theorem.
Guided GUI testing of android apps with minimal restart and approximate learning
Authors: Choi Wontae , Necula George , Sen Koushik
Published: November 2013

Smartphones and tablets with rich graphical user interfaces (GUI) are becoming increasingly popular. Hundreds of thousands of specialized applications, called apps, are available for such mobile platforms. Manual testing is the most popular technique for testing graphical user interfaces of such apps. Manual testing is often tedious and error-prone. In this paper, we propose an automated technique, called
Swift-Hand
, for generating sequences of test inputs for Android apps. The technique uses machine learning to learn a model of the app during testing, uses the learned model to generate user inputs that visit unexplored states of the app, and uses the execution of the app on the generated inputs to refine the model. A key feature of the testing algorithm is that it avoids restarting the app, which is a significantly more expensive operation than executing the app on a sequence of inputs. An important insight behind our testing algorithm is that we do not need to learn a precise model of an app, which is often computationally intensive, if our goal is to simply guide test execution into unexplored parts of the state space. We have implemented our testing algorithm in a publicly available tool for Android apps written in Java. Our experimental results show that we can achieve significantly better coverage than traditional random testing and L*-based testing in a given time budget. Our algorithm also reaches peak coverage faster than both random and L*-based testing.
Efficient divide-and-conquer parsing of practical context-free languages
Authors: Bernardy Jean-Philippe , Claessen Koen
Published: November 2013

We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is
O
(
n
3
) in the worst case, it improves to
O
(log
n
3
), under certain conditions satisfied by many useful inputs. These conditions occur for example in program texts written by humans. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms can be parallelized relatively easily.
Type-theory in color
Authors: Bernardy Jean-Philippe , Guilhem Moulin
Published: November 2013

Dependent type-theory aims to become the standard way to formalize mathematics at the same time as displacing traditional platforms for high-assurance programming. However, current implementations of type theory are still lacking, in the sense that some obvious truths require explicit proofs, making type-theory awkward to use for many applications, both in formalization and programming. In particular, notions of erasure are poorly supported.

In this paper we propose an extension of type-theory with colored terms, color erasure and interpretation of colored types as predicates. The result is a more powerful type-theory: some definitions and proofs may be omitted as they become trivial, it becomes easier to program with precise types, and some parametricity results can be internalized.
Unifying structured recursion schemes
Authors: Hinze Ralf , Wu Nicolas , Gibbons Jeremy
Published: November 2013

Folds over inductive datatypes are well understood and widely used. In their plain form, they are quite restricted; but many disparate generalisations have been proposed that enjoy similar calculational benefits. There have also been attempts to unify the various generalisations: two prominent such unifications are the 'recursion schemes from comonads' of Uustalu, Vene and Pardo, and our own 'adjoint folds'. Until now, these two unified schemes have appeared incompatible. We show that this appearance is illusory: in fact, adjoint folds subsume recursion schemes from comonads. The proof of this claim involves standard constructions in category theory that are nevertheless not well known in functional programming: Eilenberg-Moore categories and bialgebras.
Complete and easy bidirectional typechecking for higher-rank polymorphism
Authors: Dunfield Jana , Krishnaswami Neelakantan R.
Published: November 2013

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as eta-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete.
Functional reactive programming with liveness guarantees
Authors: Jeffrey Alan
Published: November 2013

Functional Reactive Programming (FRP) is an approach to the development of reactive systems which provides a pure functional interface, but which may be implemented as an abstraction of an imperative event-driven layer. FRP systems typically provide a model of behaviours (total time-indexed values, implemented as pull systems) and event sources (partial time-indexed values, implemented as push systems). In this paper, we investigate a type system for event-driven FRP programs which provide liveness guarantees, that is every input event is guaranteed to generate an output event. We show that FRP can be implemented on top of a model of sets and relations, and that the isomorphism between event sources and behaviours corresponds to the isomorphism between relations and set-valued functions. We then implement sets and relations using a model of continuations using the usual double-negation CPS transform. The implementation of behaviours as pull systems based on futures, and of event sources as push systems based on the observer pattern, thus arises from first principles. We also discuss a Java implementation of the FRP model.
A practical theory of language-integrated query
Authors: Cheney James , Lindley Sam , Wadler Philip
Published: November 2013

Language-integrated query is receiving renewed attention, in part because of its support through Microsoft's LINQ framework. We present a practical theory of language-integrated query based on quotation and normalisation of quoted terms. Our technique supports join queries, abstraction over values and predicates, composition of queries, dynamic generation of queries, and queries with nested intermediate data. Higher-order features prove useful even for constructing first-order queries. We prove a theorem characterising when a host query is guaranteed to generate a single SQL query. We present experimental results confirming our technique works, even in situations where Microsoft's LINQ framework either fails to produce an SQL query or, in one case, produces an avalanche of SQL queries.
Handlers in action
Authors: Kammar Ohad , Lindley Sam , Oury Nicolas
Published: November 2013

Plotkin and Pretnar's handlers for algebraic effects occupy a sweet spot in the design space of abstractions for effectful computation. By separating effect signatures from their implementation, algebraic effects provide a high degree of modularity, allowing programmers to express effectful programs independently of the concrete interpretation of their effects. A handler is an interpretation of the effects of an algebraic computation. The handler abstraction adapts well to multiple settings: pure or impure, strict or lazy, static types or dynamic types. This is a position paper whose main aim is to popularise the handler abstraction. We give a gentle introduction to its use, a collection of illustrative examples, and a straightforward operational semantics. We describe our Haskell implementation of handlers in detail, outline the ideas behind our OCaml, SML, and Racket implementations, and present experimental results comparing handlers with existing code.
Wellfounded recursion with copatterns
Authors: Abel Andreas M. , Pientka Brigitte
Published: November 2013

In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Building on our prior work, finite data such as finite lists and trees are defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. In this work, we take a type-based approach to strong normalization by tracking size information about finite and infinite data in the type. This guarantees compositionality. More importantly, the duality of pattern and copatterns provide a unifying semantic concept which allows us for the first time to elegantly and uniformly support both well-founded induction and coinduction by mere rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such our system allows for non-determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-centric infinite data in proof assistants such as Coq and Agda.
The bedrock structured programming system
Authors: Chlipala Adam
Published: November 2013

We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.
Hoare-style reasoning with (algebraic) continuations
Authors: Delbianco Germán Andrés , Nanevski Aleksandar
Published: November 2013

Continuations are programming abstractions that allow for manipulating the "future" of a computation. Amongst their many applications, they enable implementing unstructured program flow through higher-order control operators such as callcc. In this paper we develop a Hoare-style logic for the verification of programs with higher-order control, in the presence of dynamic state. This is done by designing a dependent type theory with first class callcc and abort operators, where pre- and postconditions of programs are tracked through types. Our operators are algebraic in the sense of Plotkin and Power, and Jaskelioff, to reduce the annotation burden and enable verification by symbolic evaluation. We illustrate working with the logic by verifying a number of characteristic examples.
Modular and automated type-soundness verification for language extensions
Authors: Lorenzen Florian , Erdweg Sebastian
Published: November 2013

Language extensions introduce high-level programming constructs that protect programmers from low-level details and repetitive tasks. For such an abstraction barrier to be sustainable, it is important that no errors are reported in terms of generated code. A typical strategy is to check the original user code prior to translation into a low-level encoding, applying the assumption that the translation does not introduce new errors. Unfortunately, such assumption is untenable in general, but in particular in the context of extensible programming languages, such as Racket or SugarJ, that allow regular programmers to define language extensions.

In this paper, we present a formalism for building and automatically verifying the type-soundness of syntactic language extensions. To build a type-sound language extension with our formalism, a developer declares an extended syntax, type rules for the extended syntax, and translation rules into the (possibly further extended) base language. Our formalism then validates that the user-defined type rules are sufficient to guarantee that the code generated by the translation rules cannot contain any type errors. This effectively ensures that an initial type check prior to translation precludes type errors in generated code. We have implemented a core system in PLT Redex and we have developed a syntactically extensible variant of System F
w
that we extend with let notation, monadic do blocks, and algebraic data types. Our formalism verifies the soundness of each extension automatically.
Programming with permissions in Mezzo
Authors: Pottier François , Protzenko Jonathan
Published: November 2013

We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. This rules out certain mistakes, including representation exposure and data races, and enables new idioms, such as gradual initialization, memory re-use, and (type)state changes. Although the core static discipline disallows sharing a mutable data structure, Mezzo offers several ways of working around this restriction, including a novel dynamic ownership control mechanism which we dub "adoption and abandon".
Automatic SIMD vectorization for Haskell
Authors: Petersen Leaf , Orchard Dominic , Glew Neal
Published: November 2013

Expressing algorithms using immutable arrays greatly simplifies the challenges of automatic SIMD vectorization, since several important classes of dependency violations cannot occur. The Haskell programming language provides libraries for programming with immutable arrays, and compiler support for optimizing them to eliminate the overhead of intermediate temporary arrays. We describe an implementation of automatic SIMD vectorization in a Haskell compiler which gives substantial vector speedups for a range of programs written in a natural programming style. We compare performance with that of programs compiled by the Glasgow Haskell Compiler.
Weak optimality, and the meaning of sharing
Authors: Balabonski Thibaut
Published: November 2013

In this paper we investigate laziness and optimal evaluation strategies for functional programming languages. We consider the weak lambda-calculus as a basis of functional programming languages, and we adapt to this setting the concepts of optimal reductions that were defined for the full lambda-calculus. We prove that the usual implementation of call-by-need using sharing is optimal, that is, normalizing any lambda-term with call-by-need requires exactly the same number of reduction steps as the shortest reduction sequence in the weak lambda-calculus without sharing. Furthermore, we prove that optimal reduction sequences without sharing are not computable. Hence sharing is the only computable means to reach weak optimality.
Structural recursion for querying ordered graphs
Authors: Hidaka Soichiro , Asada Kazuyuki , Hu Zhenjiang , Kato Hiroyuki , Nakano Keisuke
Published: November 2013

Structural recursion, in the form of, for example, folds on lists and catamorphisms on algebraic data structures including trees, plays an important role in functional programming, by providing a systematic way for constructing and manipulating functional programs. It is, however, a challenge to define structural recursions for graph data structures, the most ubiquitous sort of data in computing. This is because unlike lists and trees, graphs are essentially not inductive and cannot be formalized as an initial algebra in general. In this paper, we borrow from the database community the idea of structural recursion on how to restrict recursions on infinite unordered regular trees so that they preserve the finiteness property and become terminating, which are desirable properties for query languages. We propose a new graph transformation language called lambdaFG for transforming and querying ordered graphs, based on the well-defined bisimulation relation on ordered graphs with special epsilon-edges. The language lambdaFG is a higher order graph transformation language that extends the simply typed lambda calculus with graph constructors and more powerful structural recursions, which is extended for transformations on the sibling dimension. It not only gives a general framework for manipulating graphs and reasoning about them, but also provides a solution to the open problem of how to define a structural recursion on ordered graphs, with the help of the bisimilarity for ordered graphs with epsilon-edges.
Computer science as a school subject
Authors: Peyton Jones Simon
Published: November 2013

Computer science is one of the richest, most exciting disciplines on the planet, yet any teenager will tell you that ICT (as it is called in UK schools --- "information and communication technology") is focused almost entirely on the use and application of computers, and in practice covers nothing about how computers work, nor programming, nor anything of the discipline of computer science as we understand it. Over the last two decades, computing at school has drifted from writing adventure games on the BBC Micro to writing business plans in Excel.

This is bad for our young people's education, and it is bad for our economy. Nor is this phenomenon restricted to the UK: many countries are struggling with the same issues. Our young people should be educated not only in the application and use of digital technology, but also in how it works, and its foundational principles. Lacking such knowledge renders them powerless in the face of complex and opaque technology, disenfranchises them from making informed decisions about the digital society, and deprives our nations of a well-qualified stream of students enthusiastic and able to envision and design new digital systems.

Can anything be done, given the enormous inertia of our various countries' educational systems? Sometimes, yes. After a decade of stasis, change has come to the UK. Over the last 18 months, there has been a wholesale reform of the English school computing curriculum, and substantial movement in Scotland and Wales. It now seems likely that computer science will, for the first time, become part of every child's education. This change has been driven not by institutions or by the government, but by a grass-roots movement of parents, teachers, university academics, software developers, and others. A key agent in this grass-roots movement---although not the only one---is the Computing At School Working Group (CAS).

In this talk I will describe how CAS was born and developed, and the radical changes that have taken place since in the UK. I hope that this may be encouraging for those pushing water uphill in other parts of the world, and I will also try to draw out some lessons from our experience that may be useful to others.
Verified decision procedures for MSO on words based on derivatives of regular expressions
Authors: Traytel Dmitriy , Nipkow Tobias
Published: November 2013

Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g. automata). This paper presents a verified functional decision procedure for MSO formulas that is not based on automata but on regular expressions. Functional languages are ideally suited for this task: regular expressions are data types and functions on them are defined by pattern matching and recursion and are verified by structural induction.

Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Our results have been formalized and verified in the theorem prover Isabelle. Using Isabelle's code generation facility, this yields purely functional, formally verified programs that decide equivalence of MSO formulas.
Experience report
Authors: Petersen Christian L. , Gorges Matthias , Dunsmuir Dustin , Ansermino Mark , Dumont Guy A.
Published: November 2013

A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. The system is based on the portable Gambit Scheme programming language and provides a flexible cross-platform environment for developing graphical applications on mobile devices as well as medical instrumentation interfaces running on embedded platforms. Real world applications of this framework for mobile diagnostics, telemonitoring and automated drug infusions are reported. The source code for the core framework is open source and available at: https://github.com/part-cw/lambdanative.
Multi-core composability in the face of memory-bus contention
Authors: Behnam Moris , Inam Rafia , Nolte Thomas , Sjödin Mikael
Published: November 2013

In this paper we describe the problem of achieving composability of independently developed real-time subsystems to be executed on a multi-core platform, and we provide a solution to tackle it. We evaluate existing work for achieving real-time predictability on multi-cores and illustrate their lack with respect to composability.

To address composability we present a multi-resource server-based scheduling technique to provide predictable performance when composing multiple subsystems on a shared multi-core platform. To achieve composability on multi-core platforms, we propose to add memory bandwidth as an additional server resource. Tasks within our multi-resource servers are guaranteed both CPU- and memory bandwidth; thus the performance of a server will become independent of resource usage by tasks in other servers. We are currently implementing multi-resource servers for the Enea OSE operating system for a Freescale P4080 8-core processor, to be tested with software for a 3G-basestation.
Consumer Fronts, Global Change, and Runaway Collapse in Ecosystems
Authors: Silliman Brian R. , McCoy Michael W. , Angelini Christine , Holt Robert D. , Griffin John N. , van de Koppel Johan
Published: November 2013

Consumer fronts occur when grazers or predators aggregate in bands along the edges of a resource. Our review reveals that consumer fronts are a common phenomenon in nature, occur in many different ecosystems, and are triggered by universal mechanisms: External forces locally increase top-down control beyond prey carrying and/or renewal capacity, and resource-dependent movement leads to consumer aggregation along the edge of the remaining prey population. Once formed, consumer fronts move through systems as spatially propagating waves, self-reinforced via intense overexploitation and amplified by density-dependent feedbacks. When consumer fronts are spatially restricted, they generate patchiness. In contrast, when consumer fronts are expansive, they can lead to runaway responses that cause large-scale ecosystem degradation and regime shifts. We conceptualize a synergistic stress hypothesis and model that highlight how coupled intensification of physical stress and enhanced consumer pressure can trigger increased occurrence of consumer fronts and decreased system stability and resilience. With escalating climate change and food-web modification, the physical and biological conditions favoring consumer-front formation will likely become a common feature of many ecosystems.
Genotype-by-Environment Interaction and Plasticity: Exploring Genomic Responses of Plants to the Abiotic Environment
Authors: Des Marais David L. , Hernandez Kyle M. , Juenger Thomas E.
Published: November 2013

There is considerable interest in the occurrence and molecular mechanisms of phenotypic plasticity and genotype-by-environment interactions (G×E) in plant populations. The emergence of genomic tools, including quantitative trait locus (QTL) mapping and transcriptome studies, provides opportunities to identify G×E patterns and mechanisms across a diversity of phenotypes, species, and environments. We review progress in evaluating the presence and characterizing the mechanisms of G×E using genomic studies of abiotic responses in plants. Our review reveals that G×E is common, often caused by changes in the magnitude of genetic effects in response to the environment, and associated with diverse genetic factors and molecular variants. We illustrate this diversity with an examination of transcriptome studies and discussion of cloned genes underlying G×E. We discuss the caveats associated with existing studies and outline future directions for better understanding G×E and its impact on local adaptation and plant improvement.
RNA Editing in Plants and Its Evolution
Authors: Takenaka Mizuki , Zehrmann Anja , Verbitskiy Daniil , Härtel Barbara , Brennicke Axel
Published: November 2013

RNA editing alters the identity of nucleotides in RNA molecules such that the information for a protein in the mRNA differs from the prediction of the genomic DNA. In chloroplasts and mitochondria of flowering plants, RNA editing changes C nucleotides to U nucleotides; in ferns and mosses, it also changes U to C. The approximately 500 editing sites in mitochondria and 40 editing sites in plastids of flowering plants are individually addressed by specific proteins, genes for which are amplified in plant species with organellar RNA editing. These proteins contain repeat elements that bind to cognate RNA sequence motifs just 5′ to the edited nucleotide. In flowering plants, the site-specific proteins interact selectively with individual members of a different, smaller family of proteins. These latter proteins may be connectors between the site-specific proteins and the as yet unknown deaminating enzymatic activity.
Detecting Natural Selection in Genomic Data
Authors: Vitti Joseph J. , Grossman Sharon R. , Sabeti Pardis C.
Published: November 2013

The past fifty years have seen the development and application of numerous statistical methods to identify genomic regions that appear to be shaped by natural selection. These methods have been used to investigate the macro- and microevolution of a broad range of organisms, including humans. Here, we provide a comprehensive outline of these methods, explaining their conceptual motivations and statistical interpretations. We highlight areas of recent and future development in evolutionary genomics methods and discuss ongoing challenges for researchers employing such tests. In particular, we emphasize the importance of functional follow-up studies to characterize putative selected alleles and the use of selection scans as hypothesis-generating tools for investigating evolutionary histories.
Pathogenesis of Abdominal Aortic Aneurysms: MicroRNAs, Proteases, Genetic Associations
Authors: Maegdefessel Lars , Dalman Ronald L. , Tsao Philip S.
Published: November 2013

Abdominal aortic aneurysm (AAA) disease is a common, morbid, and highly lethal pathology. Extraordinary efforts have been launched to determine the molecular and pathophysiological characteristics of AAAs. Although surgery is highly effective in preventing death by rupture for larger AAAs, no guidance or preventive therapy is currently available for the >90% of patients whose aneurysms are below the surgical threshold. Predictive animal models of AAA as well as human pathological samples have revealed a complex circuit of AAA formation and progression. The proteolytic destruction of matrix components of the aorta by different proteases has been extensively studied over many years. Recently, a novel class of small noncoding RNAs, called microRNAs, was identified as “fine-tuners” of the translational output of target genes; they act by promoting mRNA degradation. Their therapeutic potential in limiting AAA development appears very intriguing. Further, current studies assessing genetic and heritable associations for AAA disease have provided great insight into its pathogenesis, potentially enabling us to better clinically manage affected patients.
Inflammasomes and Metabolic Disease
Authors: Henao-Mejia Jorge , Elinav Eran , Thaiss Christoph A. , Flavell Richard A.
Published: November 2013

Innate immune response pathways and metabolic pathways are evolutionarily conserved throughout species and are fundamental to survival. As such, the regulation of whole-body and cellular metabolism is intimately integrated with immune responses. However, the introduction of new variables to this delicate evolutionarily conserved physiological interaction can lead to deleterious consequences for organisms as a result of inappropriate immune responses. In recent decades, the prevalence and incidence of metabolic diseases associated with obesity have dramatically increased worldwide. As a recently acquired human characteristic, obesity has exposed the critical role of innate immune pathways in multiple metabolic pathophysiological processes. Here, we review recent evidence that highlights inflammasomes as critical sensors of metabolic perturbations in multiple tissues and their role in the progression of highly prevalent metabolic diseases.
Advanced Harmony Search with Ant Colony Optimization for Solving the Traveling Salesman Problem
Authors: Yun Ho-Yoeng , Jeong Suk-Jae , Kim Kyung-Sup
Published: November 2013

We propose a novel heuristic algorithm based on the methods of advanced Harmony Search and Ant Colony Optimization (AHS-ACO) to effectively solve the Traveling Salesman Problem (TSP). The TSP, in general, is well known as an NP-complete problem, whose computational complexity increases exponentially by increasing the number of cities. In our algorithm, Ant Colony Optimization (ACO) is used to search the local optimum in the solution space, followed by the use of the Harmony Search to escape the local optimum determined by the ACO and to move towards a global optimum. Experiments were performed to validate the efficiency of our algorithm through a comparison with other algorithms and the optimum solutions presented in the TSPLIB. The results indicate that our algorithm is capable of generating the optimum solution for most instances in the TSPLIB; moreover, our algorithm found better solutions in two cases (kroB100 and pr144) when compared with the optimum solution presented in the TSPLIB.
Shape Reconstruction of Thin Electromagnetic Inclusions via Boundary Measurements: Level-Set Method Combined with the Topological Derivative
Authors: Park Won-Kwang
Published: November 2013

An inverse problem for reconstructing arbitrary-shaped thin penetrable electromagnetic inclusions concealed in a homogeneous material is considered in this paper. For this purpose, the level-set evolution method is adopted. The topological derivative concept is incorporated in order to evaluate the evolution speed of the level-set functions. The results of the corresponding numerical simulations with and without noise are presented in this paper.
A Direct Eulerian GRP Scheme for the Prediction of Gas-Liquid Two-Phase Flow in HTHP Transient Wells
Authors: Xu Jiuping , Luo Min , Hu Jiancheng , Wang Shize , Qi Bin , Qiao Zhiguo
Published: November 2013

A coupled system model of partial differential equations is presented in this paper, which concerns the variation of the pressure and temperature, velocity, and density at different times and depths in high temperature-high pressure (HTHP) gas-liquid two-phase flow wells. A new dimensional splitting technique with Eulerian generalized riemann problem (GRP) scheme is applied to solve this set of conservation equations, where Riemann invariants are introduced as the main ingredient to resolve the generalized Riemann problem. The basic data of “X well” (HTHP well), 7100 m deep, located in Southwest China, is used for the case history calculations. Curve graphs of pressures and temperatures along the depth of the well are plotted at different times. The comparison with the results of Lax Friedrichs (LxF) method shows that the calculating results are more fitting to the values of real measurement and the new method is of high accuracy.
The Cardioprotective Effect of Hypertonic Saline Is Associated with Inhibitory Effect on Macrophage Migration Inhibitory Factor in Sepsis
Authors: Wang Yi-Li , Lam Kwok-Keung , Cheng Pao-Yun , Kung Ching-Wen , Chen Shu-Ying , Chao Chun-Chih , Hwang Hwong-Ru , Chung Ming-Ting , Lee Yen-Mei
Published: November 2013

Sepsis can cause myocardial dysfunction, which contributes to the high mortality of sepsis. Hypertonic saline (HS) has been reported to increase myocardial contractility in sepsis. In the present study, mechanisms of action of HS resuscitation (4 mL of 7.5% NaCl per kilogram) on cardiac function have been evaluated in septic rats. HS was administered 1 h after LPS (10 mg/kg, i.v.) challenge. The mean arterial blood pressure significantly decreased 4 h after LPS challenge, and septic shock was observed at the end of experiment (6 h). Posttreatment with HS prevented hypotension caused by LPS and significantly improved cardiac function, evidenced by increases in left ventricular developed pressure, mean+dP/dtand-dP/dt. The amplitude of electrical-stimulated intracellular Ca2+transient in isolated single cardiomyocytes was significantly reduced after 6 h LPS insult, which was recovered by HS. In addition, LPS resulted in significant increases in neutrophil myeloperoxidase activity, macrophage migration inhibitory factor (MIF), and NF-κB phospho-p65 protein levels in myocardium at 6 h, which were significantly attenuated by HS. In conclusion, HS improved myocardial contractility and prevented circulatory failure induced by endotoxemia, which may attribute to improvement of intracellular calcium handling process and inhibitory effects on neutrophil infiltration and MIF production in hearts.
An Ensemble Method for High-Dimensional Multilabel Data
Authors: Liu Huawen , Zheng Zhonglong , Zhao Jianmin , Ye Ronghua
Published: November 2013

Multilabel learning is now receiving an increasing attention from a variety of domains and many learning algorithms have been witnessed. Similarly, the multilabel learning may also suffer from the problems of high dimensionality, and little attention has been paid to this issue. In this paper, we propose a new ensemble learning algorithms for multilabel data. The main characteristic of our method is that it exploits the features with local discriminative capabilities for each label to serve the purpose of classification. Specifically, for each label, the discriminative capabilities of features on positive and negative data are estimated, and then the top features with the highest capabilities are obtained. Finally, a binary classifier for each label is constructed on the top features. Experimental results on the benchmark data sets show that the proposed method outperforms four popular and previously published multilabel learning algorithms.
Thin-Film LSCs Based on PMMA Nanohybrid Coatings: Device Optimization and Outdoor Performance
Authors: El-Bashir S. M. , AlHarbi O. A. , AlSalhi M. S.
Published: November 2013

This study concerns the design optimization of thin-film luminescent solar concentrators (TLSCs) based on polymethylmethacrylate (PMMA)/silica nanohybrid films doped with coumarin dyestuffs specialized in coloring plastics. Two designs of TLSCs had been prepared and characterized. The first consists of a transparent nanohybrid layer coated on a fluorescent PMMA substrate. The second design is the ordinary configuration in which fluorescent nanohybrid layer is coated on a transparent PMMA substrate. The investigation of the spectral properties and efficiency parameters recommended the best solar energy conversion efficiency for the second design. The outdoor performance of optimized TLSC was also evaluated under clear sky conditions of Riyadh city, and the hourly values of the optical efficiency,ηopt, were calculated for one year. The best performance was achieved in summer since the short circuit current for PV cell was doubled after being attached to TLSC and the value ofηoptreached 40% which is higher than other values recorded before due to the abundant solar energy potential in the Arabian Peninsula.
Vibration Characteristics of Gravity-Type Caisson Breakwater Structure with Water-Level Variation
Authors: Lee So-Young , Huynh Thanh-Canh , Kim Jeong-Tae , Yoon Han-Sam , Han Sang-Hun
Published: November 2013

Vibration characteristics of gravity-type caisson breakwater structures which have water-level variations are experimentally examined by using wave load excitations. To achieve the objective, the following approaches are implemented. Firstly, vibration analysis methods are selected to examine the dynamic characteristics of the lab-scale caisson. Secondly, vibration test on a lab-scale caisson which is installed in a two-dimensional wave flume is performed under several excitation sources and water levels. Thirdly, the compatibility of the wave-induced vibration responses is evaluated by comparison with the impact vibration responses, and the appropriate vibration analysis method is selected. Finally, the water-level effects on the caisson breakwater are examined based on the modal parameters which are experimentally measured for the 2D wave flume tests.
Level Set Based Coverage Holes Detection and Holes Healing Scheme in Hybrid Sensor Network
Authors: Yu Xiaosheng , Wu Chengdong , Chen Dongyue , Hu Nan
Published: November 2013

A fundamental issue in sensor network is the coverage problem. Since the distribution of sensor nodes is not usually uniform due to random deployment and node failures, the coverage holes are hardly avoided in sensor network. And the coverage holes are important health indicators of the sensor network. This paper firstly proposes a level set based coverage holes detection algorithm for hybrid sensor network. This algorithm could estimate the number of holes and the size of the holes. Then we propose genetic algorithms based coverage holes healing algorithm. This algorithm could leverage mobility to optimize the average coverage rate and the average movement distance of the mobile nodes. Simulation results show that the proposed method could detect the holes efficiently. The holes healing algorithm outperforms the Random and Delaunay methods.
Propofol Reduces Lipopolysaccharide-Induced, NADPH Oxidase (NOX2) Mediated TNF-αand IL-6 Production in Macrophages
Authors: Meng Tao , Yu Jingya , Lei Zhen , Wu Jianbo , Wang Shuqin , Bo Qiyu , Zhang Xinyu , Ma Zhiyong , Yu Jingui
Published: November 2013

During an infection, lipopolysaccharide (LPS) stimulates the production of reactive oxygen species (ROS), which is mediated, in large part, by nicotinamide adenine dinucleotide phosphate (NADPH) oxidases (NOXs); NOX2is the major NOX isoform found in the macrophage cell membrane. While the immunomodulatory activity of propofol is highly documented, its effect on the LPS-induced NOX2/ROS/NF-κB signaling pathway in macrophages has not been addressed. In present study, we used murine macrophage cell line RAW264.7 pretreated with propofol and stimulated with LPS. IL-6 and TNF-αexpression, ROS production, and NOX activity were determined. Results showed that propofol attenuated LPS-induced TNF-αand IL-6 expression. Moreover, LPS-stimulated phosphorylation of NF-κB and generation of ROS were weakened in response to propofol. Propofol also reduced LPS-induced NOX activity and expression of gp91phox and p47phox. We conclude that propofol modulates LPS signaling in macrophages by reducing NOX-mediated production of TNF-αand IL-6.
Resistance Switching Characteristics in ZnO-Based Nonvolatile Memory Devices
Authors: Chiu Fu-Chien
Published: November 2013

Bipolar resistance switching characteristics are demonstrated in Pt/ZnO/Pt nonvolatile memory devices. A negative differential resistance or snapback characteristic can be observed when the memory device switches from a high resistance state to a low resistance state due to the formation of filamentary conducting path. The dependence of pulse width and temperature on set/reset voltages was examined in this work. The exponentially decreasing trend of set/reset voltage with increasing pulse width is observed except when pulse width is larger than 1 s. Hence, to switch the ZnO memory devices, a minimum set/reset voltage is required. The set voltage decreases linearly with the temperature whereas the reset voltage is nearly temperature-independent. In addition, the ac cycling endurance can be over 106switching cycles, whereas, the dependence of HRS/LRS resistance distribution indicates that a significant memory window closure may take place after about 102  dc switching cycles.
Phytochemistry, Pharmacology and Toxicology ofSpilanthes acmella: A Review
Authors: Dubey Suchita , Maity Siddhartha , Singh Mahendra , Saraf Shubhini A. , Saha Sudipta
Published: November 2013

Spilanthes acmellais an important medicinal plant, found in tropical and subtropical countries mainly India and South America. Popularly, it is known as toothache plant which reduces the pain associated with toothaches and can induce saliva secretion. Various extracts and active metabolites from various parts of this plant possess useful pharmacological activities. Literature survey proposed that it has multiple pharmacological actions, which include antifungal, antipyretic, local anaesthetic, bioinsecticide, anticonvulsant, antioxidant, aphrodisiac, analgesic, pancreatic lipase inhibitor, antimicrobial, antinociception, diuretic, vasorelaxant, anti-human immunodeficiency virus, toothache relieve and anti-inflammatory effects. This review is elaborately describing the traditional uses, phytochemistry, pharmacology, and toxicology of this plant. This review would assist researchers to search scientific information in the future.