bluuebunny/crossref_metadata_2025 huggingface dataset:
Epidemiology and Virulence of
Klebsiella pneumoniae
Authors: Clegg Steven , Murphy Caitlin N.
Published: April 2016

Strains of
Klebsiella pneumoniae
are frequently opportunistic pathogens implicated in urinary tract and catheter-associated urinary-tract infections of hospitalized patients and compromised individuals. Infections are particularly difficult to treat since most clinical isolates exhibit resistance to several antibiotics leading to treatment failure and the possibility of systemic dissemination. Infections of medical devices such as urinary catheters is a major site of
K. pneumoniae
infections and has been suggested to involve the formation of biofilms on these surfaces. Over the last decade there has been an increase in research activity designed to investigate the pathogenesis of
K. pneumoniae
in the urinary tract. These investigations have begun to define the bacterial factors that contribute to growth and biofilm formation. Several virulence factors have been demonstrated to mediate
K. pneumoniae
infectivity and include, but are most likely not limited to, adherence factors, capsule production, lipopolysaccharide presence, and siderophore activity. The development of both
in vitro
and
in vivo
models of infection will lead to further elucidation of the molecular pathogenesis of
K. pneumoniae
. As for most opportunistic infections, the role of host factors as well as bacterial traits are crucial in determining the outcome of infections. In addition, multidrug-resistant strains of these bacteria have become a serious problem in the treatment of
Klebsiella
infections and novel strategies to prevent and inhibit bacterial growth need to be developed. Overall, the frequency, significance, and morbidity associated with
K. pneumoniae
urinary tract infections have increased over many years. The emergence of these bacteria as sources of antibiotic resistance and pathogens of the urinary tract present a challenging problem for the clinician in terms of management and treatment of individuals.
Pathoadaptive Mutations in Uropathogenic
Escherichia coli
Authors: Sokurenko Evgeni
Published: April 2016

Uropathogenic
Escherichia coli
(UPEC) are opportunistic human pathogens that primarily circulate as part of commensal intestinal microbiota. Though they have the ability to survive and proliferate in various urinary tract compartments, the urinary tract is a transient, occasional habitat for UPEC. Because of this, most of the UPEC traits have originally evolved to serve in intestinal colonization and transmission. Some of these bacterial traits serve as virulence factors – they are critical to or assist in survival of UPEC as pathogens, and the structure and/or function may be specialized for the infection. Other traits could serve as anti-virulence factors – they represent liability in the urinary tract and are under selection to be lost or inactivated during the infection. Inactivation, variation, or other changes of the bacterial genes that increase the pathogen’s fitness during the infection are called
pathoadaptive mutations
. This chapter describes examples of pathoadaptive mutations in UPEC and provides rationale for their further in-depth study.
Antigenic Variation in Bacterial Pathogens
Authors: Palmer Guy H. , Bankhead Troy , Seifert H. Steven
Published: April 2016

Antigenic variation is a strategy used by a broad diversity of microbial pathogens to persist within the mammalian host. Whereas viruses make use of a minimal proofreading capacity combined with large amounts of progeny to use random mutation for variant generation, antigenically variant bacteria have evolved mechanisms which use a stable genome, which aids in protecting the fitness of the progeny. Here, three well-characterized and highly antigenically variant bacterial pathogens are discussed:
Anaplasma, Borrelia
, and
Neisseria
. These three pathogens display a variety of mechanisms used to create the structural and antigenic variation needed for immune escape and long-term persistence. Intrahost antigenic variation is the focus; however, the role of these immune escape mechanisms at the population level is also presented.
Basilar artery occlusion in a child treated successfully with mechanical thrombectomy using ADAPT
Authors: Lena Jonathan , Eskandari Ramin , Infinger Libby , Fargen Kyle M , Spiotta Alejandro , Turk Aquilla , Turner Raymond D , Chaudry Imran
Published: April 2016

Acute ischemic stroke (AIS) in the pediatric population is rare. Furthermore, it is common for physicians to take significantly longer diagnosing a posterior circulation stroke in a child than in an adult. There are increasing case reports in the literature of treating AIS in children with intravenous tissue plasminogen activator, intra-arterial thrombolysis, and/or mechanical thrombectomy. We present the first case of pediatric AIS treated using a direct aspiration first pass technique (ADAPT) as a means of mechanical thrombectomy.
The use of fluoxetine by veterinarians in dogs and cats: a preliminary survey
Authors: Kaur Gagandeep , Voith Victoria L. , Schmidt Peggy L.
Published: April 2016

Objective

To describe the prescribing habits of a sample of small animal veterinarians pertaining to use of fluoxetine in dogs and cats.

Design

Exploratory descriptive survey using a questionnaire, available on paper and through email, distributed to small animal veterinarians by convenience sampling.

Participants

Veterinarians practicing small animal medicine in North America contacted by email and at local veterinary meetings.

Results

Of 127 initial respondents, 106 prescribed fluoxetine for dogs and/or cats. The majority (91 per cent) indicated the drug be given once every 24 hours. Respondents used one or more formulations of fluoxetine. Of those who prescribed fluoxetine for both dogs and cats (57 per cent), 80 per cent used a generic form. A third prescribed fluoxetine only for dogs (31 per cent) and 72 per cent of these prescribed the US Food and Drug Administration approved product that was available at that time. The primary use of fluoxetine was related to behaviour problems. Overall for dogs, uses of fluoxetine were organised into five major categories by the investigators: Anxieties, Aggression, Compulsive Disorders, Phobias/Fear and Other, Anxieties being the most common. Of those who prescribed fluoxetine, 12 per cent did so only for cats and the majority of these prescribed generic (58 per cent) and or compounded (42 per cent) forms. Overall for cats, uses of fluoxetine were organised into six major categories: Elimination behaviours, Anxieties, Aggression, Dermatologic/Grooming, Compulsive Disorders and Other, Elimination behaviours being most common.

Conclusions

This study indicates that practitioners prescribed fluoxetine in generic, proprietary and compounded formulations for a variety of behaviour problems of dogs and cats. The broad use by the respondents suggests how important psychotropic drugs are in veterinary medicine. Research, information and continuing education regarding such drugs and animal behaviour should be made available to the general practitioner.
Antimicrobial properties of cultivable bacteria associated with seaweeds in the Gulf of Mannar on the southeast coast of India
Authors: Thilakan B. , Chakraborty K. , Chakraborty R.D.
Published: April 2016

In this study, 234 bacterial strains were isolated from 7 seaweed species in the Gulf of Mannar on the southeast coast of India. The strains having consistent antimicrobial activity were chosen for further studies, and this constituted about 9.8% of the active strains isolated. Phylogenetic analysis using 16S rDNA sequencing with the help of classical biochemical identification indicated the existence of 2 major phyla, Firmicutes and Proteobacteria. Antimicrobial activity analysis combined with the results of amplifying genes encoding for polyketide synthetase and nonribosomal peptide synthetase showed that seaweed-associated bacteria had broad-spectrum antimicrobial activity. These epibionts might be beneficial to seaweeds by limiting or preventing the development of competing or fouling bacteria. Phylogenetic analysis of ketosynthase (KS) regions with respect to the diverse range of KS domains showed that the KS domains from the candidate isolates were of Type I. The bacterial cultures retained their antimicrobial activities after plasmid curing, which further suggested that the antimicrobial activity of these isolates was not encoded by plasmid, and the genes encoding the antimicrobial product might be present within the genome. Seaweed-associated bacteria with potential antimicrobial activity suggested that the seaweed species are an ideal ecological niche harboring specific bacterial diversity representing a largely underexplored source of antimicrobial secondary metabolites.
Learning Topologies with the Growing Neural Forest
Authors: Palomo Esteban José , López-Rubio Ezequiel
Published: April 2016

In this work, a novel self-organizing model called growing neural forest (GNF) is presented. It is based on the growing neural gas (GNG), which learns a general graph with no special provisions for datasets with separated clusters. On the contrary, the proposed GNF learns a set of trees so that each tree represents a connected cluster of data. High dimensional datasets often contain large empty regions among clusters, so this proposal is better suited to them than other self-organizing models because it represents these separated clusters as connected components made of neurons. Experimental results are reported which show the self-organization capabilities of the model. Moreover, its suitability for unsupervised clustering and foreground detection applications is demonstrated. In particular, the GNF is shown to correctly discover the connected component structure of some datasets. Moreover, it outperforms some well-known foreground detectors both in quantitative and qualitative terms.
First-principles calculations for point defects in MAX phases Ti2AlN
Authors: Zhang Yaowen , Yang Shutong , Wang Canglong
Published: April 2016

This paper outlines general physical issues associated with performing computational numerical simulations of primary point defects in MAX phases Ti2AlN. First-principles solutions are possible due to the development of computational resources of software and hardware. The calculation accuracy is a good agreement with the experimental results. As an important application of our simulations, the results could provide a theoretical guidance for future experiments and application of Ti2AlN. For example, the N mono-vacancy is the most difficult to form. On the contrary, the mono-vacancy formation in Ti2AlN is energetically most favorable for the Al atom. The essence of the phenomena is explained by the calculated density of state (DOS).
Interfacial potential approach for Ag/Si(111) interface
Authors: Liu Yong-Qiang , Song Hong-Quan , Shen Jiang
Published: April 2016

By applying the Chen–Möbius inversion method, a concise formula is introduced to get the pair potentials of the Ag/Si(111) interface by inversion of the ab initio adhesive energies. The check shows that the inversed potentials are self-consistent. Then, by using the interfacial potentials obtained, we analyze the changes of the energy, stress and atomic structures, giving a detailed presentation of the fracture process about the Ag/Si(111) interface. Meanwhile, we know that there are three kinds of fracture mode. In this work, the fracture process is performed in mode II (shear).
Synthesis and characterization of NaAlSi2O6 jadeite under high pressure from 4.0 GPa to 5.5 GPa
Authors: Wang Fang Biao , Zuo Gui Hong , Wang Li Juan , Zheng You Jin , Jia Xiao Peng , Ma Hong An
Published: April 2016

The method of high pressure and high temperature (HPHT) has been used for the synthesis of jadeite. Through this method, the NaAlSi2O6 jadeite can be obtained in the pressure range of 4.0–5.5 GPa. All the experimental results reveal that the microstructure and properties of synthetic jadeite resemble the natural jadeite very much. The research indicates that the crystallization temperature of the synthesized NaAlSi2O6 jadeite rises with the increase of the pressure, which will help in gaining a deep understanding on the origin of natural jadeite.
A Different Approach to Design Non-Isolated DC–DC Converters for Maximum Power Point Tracking in Solar Photovoltaic Systems
Authors: Verma Deepak , Nema S. , Shandilya A. M.
Published: April 2016

Maximum power point tracking (MPPT) is an essential part of solar photovoltaic (PV) system to draw maximum available power which is generated by the solar PV. The concept of MPPT is based on maximum power transfer theorem. When the impedance of source is equal to the load impedance then only, source or solar PV delivers maximum power to the load. Impedance matching is done through DC–DC converter, whereas the duty cycle of the converter is decided by the MPPT algorithm. Nonetheless, DC–DC converter design is a key aspect in any tracking scheme, bulk of publications on MPPT are available in literature but very less information can be obtained on DC–DC converter design. Thus, the main focus of this paper is to provide an easy converter design procedure for MPPT in solar PV applications on the basis of solar panels impedance. In this paper, a step by step design of buck converter, boost converter and buck–boost converter particularly for MPPT applications is presented and results are verified through OPAL-RT OP4500 Real Time Simulator.
High Performance Architecture of Motion Estimation Algorithm for Video Compression
Authors: Muralidhar P. , Rao C. B. Rama
Published: April 2016

Motion estimation (ME) is a highly computationally intensive operation in video compression. Efficient ME architectures are proposed in the literature. This paper presents an efficient low computational complexity systolic architecture for full search block matching ME (FSBME) algorithm. The proposed architecture is based on one-bit transform-based full search (FS) algorithm. The proposed ME hardware architectures perform FS ME for four macroblocks (MBs) in parallel. The proposed hardware architecture is implemented in VHDL. The FSBME hardware consumes 34% of the slices in a Xilinx Vertex XC6vlx240T FPGA device with a maximum frequency of 133[Formula: see text]MHz and is capable of processing full high definition (HD) ([Formula: see text]) frames at a rate of 60 frames per second.
Low Complexity DCT Approximation for Image Compression in Wireless Image Sensor Networks
Authors: Mechouek Khaoula , Kouadria Nasreddine , Doghmane Noureddine , Kaddeche Nadia
Published: April 2016

Energy consumption is a critical problem affecting the lifetime of wireless image sensor networks (WISNs). In such systems, images are usually compressed using JPEG standard to save energy during transmission. And since DCT transformation is the most computationally intensive part in the JPEG technique, several approximation techniques have been proposed to further decrease the energy consumption. In this paper, we propose a low-complexity DCT approximation method which is based on the combination of the rounded DCT with a pruned approach. Experimental comparison with recently proposed schemes, using Atmel Atmega128L platform, shows that our method requires less arithmetic operations, and hence less processing time and/or the energy consumption while providing better performance in terms of PSNR metric.
Flexural Vibration of Prestressed Concrete Bridges with Corrugated Steel Webs
Authors: Chen Xia-Chun , Li Zhen-Hu , Au Francis T. K. , Jiang Rui-Juan
Published: April 2016

Prestressed concrete bridges with corrugated steel webs have emerged as a new form of steel-concrete composite bridges with remarkable advantages compared with the traditional ones. However, the assumption that plane sections remain plane may no longer be valid for such bridges due to the different behavior of the constituents. The sandwich beam theory is extended to predict the flexural vibration behavior of this type of bridges considering the presence of diaphragms, external prestressing tendons and interaction between the web shear deformation and flange local bending. To this end, a [Formula: see text] beam finite element is formulated. The proposed theory and finite element model are verified both numerically and experimentally. A comparison between the analyses based on the sandwich beam model and on the classical Euler–Bernoulli and Timoshenko models reveals the following findings. First of all, the extended sandwich beam model is applicable to the flexural vibration analysis of the bridges considered. By letting [Formula: see text] denote the square root of the ratio of equivalent shear rigidity to the flange local flexural rigidity, and L the span length, the combined parameter [Formula: see text] appears to be more suitable for considering the diaphragm effect and the interaction between the shear deformation and flange local bending. The diaphragms have significant effect on the flexural natural frequencies and mode shapes only when the [Formula: see text] value of the bridge falls below a certain limit. For a bridge with an [Formula: see text] value over a certain limit, the flexural natural frequencies and mode shapes obtained from the sandwich beam model and the classical Euler–Bernoulli and Timoshenko models tend to be the same. In such cases, either of the classical beam theories may be used.
Rapid generation of collagen-based microtissues to study cell–matrix interactions
Authors: Brett Marie-Elena , Crampton Alexandra L. , Wood David K.
Published: April 2016

The objective of this study was to create a method for studying cell–matrix interactions in a physiologically relevant 3D protein-based tissue construct that could be scaled up to perform large-scale screens, study cell–matrix interactions on a population basis, or be remodeled by cells to build larger tissues. We have developed an easy-to-use method to miniaturize protein-based tissue constructs that maintains the 3D in vitro environment, while alleviating several obstacles associated with larger avascular tissue constructs. In this study, we demonstrate that (i) cells can interact with the 3D environment both while encapsulated or while interacting only with the surface of the microtissues, (ii) encapsulated cells are highly viable and, for the first time, (iii) microtissues on this size scale (~200 μm) can be used to quantify cell contractility. This versatile platform should facilitate large-scale screens in 3D in vitro culture conditions for drug development and high throughput mechanistic biology.
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Authors: Dodds Mike , Jagannathan Suresh , Parkinson Matthew J. , Svendsen Kasper , Birkedal Lars
Published: April 2016

Synchronization constructs lie at the heart of any reliable concurrent program. Many such constructs are standard (e.g., locks, queues, stacks, and hash-tables). However, many concurrent applications require custom synchronization constructs with special-purpose behavior. These constructs present a significant challenge for verification. Like standard constructs, they rely on subtle racy behavior, but unlike standard constructs, they may not have well-understood abstract interfaces. As they are custom built, such constructs are also far more likely to be unreliable.

This article examines the formal specification and verification of custom synchronization constructs. Our target is a library of channels used in automated parallelization to enforce sequential behavior between program statements. Our high-level specification captures the conditions necessary for correct execution; these conditions reflect program dependencies necessary to ensure sequential behavior. We connect the high-level specification with the low-level library implementation to prove that a client’s requirements are satisfied. Significantly, we can reason about program and library correctness without breaking abstraction boundaries.

To achieve this, we use a program logic called iCAP (impredicative Concurrent Abstract Predicates) based on separation logic. iCAP supports both high-level abstraction and low-level reasoning about races. We use this to show that our high-level channel specification abstracts three different, increasingly complex low-level implementations of the library. iCAP’s support for higher-order reasoning lets us prove that sequential dependencies are respected, while iCAP’s next-generation semantic model lets us avoid ugly problems with cyclic dependencies.
Automatic patch generation by learning correct code
Authors: Long Fan , Rinard Martin
Published: April 2016

We present Prophet, a novel patch generation system that works with a set of successful human patches obtained from open- source software repositories to learn a probabilistic, application-independent model of correct code. It generates a space of candidate patches, uses the model to rank the candidate patches in order of likely correctness, and validates the ranked patches against a suite of test cases to find correct patches. Experimental results show that, on a benchmark set of 69 real-world defects drawn from eight open-source projects, Prophet significantly outperforms the previous state-of-the-art patch generation system.
Model checking for symbolic-heap separation logic with inductive predicates
Authors: Brotherston James , Gorogiannis Nikos , Kanovich Max , Rowe Reuben
Published: April 2016

We investigate the *model checking* problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g. in software testing or runtime verification. First, we show that the problem is *decidable*; specifically, we present a bottom-up fixed point algorithm that decides the problem and runs in exponential time in the size of the problem instance. Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments. Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.
Algorithms for algebraic path properties in concurrent systems of constant treewidth components
Authors: Chatterjee Krishnendu , Goharshady Amir Kafshdar , Ibsen-Jensen Rasmus , Pavlogiannis Andreas
Published: April 2016

We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.
Unboundedness and downward closures of higher-order pushdown automata
Authors: Hague Matthew , Kochems Jonathan , Ong C.-H. Luke
Published: April 2016

We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.
The gradualizer: a methodology and algorithm for generating gradual type systems
Authors: Cimini Matteo , Siek Jeremy G.
Published: April 2016

Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.
Type theory in type theory using quotient inductive types
Authors: Altenkirch Thorsten , Kaposi Ambrus
Published: April 2016

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.
Lightweight verification of separate compilation
Authors: Kang Jeehoon , Kim Yoonseung , Hur Chung-Kil , Dreyer Derek , Vafeiadis Viktor
Published: April 2016

Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple "closed simulations" used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et al. have done, involves major changes and extensions to its original verification. In this paper, we show that if we aim somewhat lower---to prove correctness of separate compilation, but only for a *single* compiler---we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler.
Reducing crash recoverability to reachability
Authors: Koskinen Eric , Yang Junfeng
Published: April 2016

Software applications run on a variety of platforms (filesystems, virtual slices, mobile hardware, etc.) that do not provide 100% uptime. As such, these applications may crash at any unfortunate moment losing volatile data and, when re-launched, they must be able to correctly recover from potentially inconsistent states left on persistent storage. From a verification perspective, crash recovery bugs can be particularly frustrating because, even when it has been formally proved for a program that it satisfies a property, the proof is foiled by these external events that crash and restart the program. In this paper we first provide a hierarchical formal model of what it means for a program to be crash recoverable. Our model captures the recoverability of many real world programs, including those in our evaluation which use sophisticated recovery algorithms such as shadow paging and write-ahead logging. Next, we introduce a novel technique capable of automatically proving that a program correctly recovers from a crash via a reduction to reachability. Our technique takes an input control-flow automaton and transforms it into an encoding that blends the capture of snapshots of pre-crash states into a symbolic search for a proof that recovery terminates and every recovered execution simulates some crash-free execution. Our encoding is designed to enable one to apply existing abstraction techniques in order to do the work that is necessary to prove recoverability. We have implemented our technique in a tool called Eleven82, capable of analyzing C programs to detect recoverability bugs or prove their absence. We have applied our tool to benchmark examples drawn from industrial file systems and databases, including GDBM, LevelDB, LMDB, PostgreSQL, SQLite, VMware and ZooKeeper. Within minutes, our tool is able to discover bugs or prove that these fragments are crash recoverable.
A theory of effects and resources: adjunction models and polarised calculi
Authors: Curien Pierre-Louis , Fiore Marcelo , Munch-Maccagnoni Guillaume
Published: April 2016

We consider the Curry-Howard-Lambek correspondence for effectful computation and resource management, specifically proposing polarised calculi together with presheaf-enriched adjunction models as the starting point for a comprehensive semantic theory relating logical systems, typed calculi, and categorical models in this context. Our thesis is that the combination of effects and resources should be considered orthogonally. Model theoretically, this leads to an understanding of our categorical models from two complementary perspectives: (i) as a linearisation of CBPV (Call-by-Push-Value) adjunction models, and (ii) as an extension of linear/non-linear adjunction models with an adjoint resolution of computational effects. When the linear structure is cartesian and the resource structure is trivial we recover Levy’s notion of CBPV adjunction model, while when the effect structure is trivial we have Benton’s linear/non-linear adjunction models. Further instances of our model theory include the dialogue categories with a resource modality of Melliès and Tabareau, and the [E]EC ([Enriched] Effect Calculus) models of Egger, Møgelberg and Simpson. Our development substantiates the approach by providing a lifting theorem of linear models into cartesian ones. To each of our categorical models we systematically associate a typed term calculus, each of which corresponds to a variant of the sequent calculi LJ (Intuitionistic Logic) or ILL (Intuitionistic Linear Logic). The adjoint resolution of effects corresponds to polarisation whereby, syntactically, types locally determine a strict or lazy evaluation order and, semantically, the associativity of cuts is relaxed. In particular, our results show that polarisation provides a computational interpretation of CBPV in direct style. Further, we characterise depolarised models: those where the cut is associative, and where the evaluation order is unimportant. We explain possible advantages of this style of calculi for the operational semantics of effects.
Scaling network verification using symmetry and surgery
Authors: Plotkin Gordon D. , Bjørner Nikolaj , Lopes Nuno P. , Rybalchenko Andrey , Varghese George
Published: April 2016

On the surface, large data centers with about 100,000 stations and nearly a million routing rules are complex and hard to verify. However, these networks are highly regular by design; for example they employ fat tree topologies with backup routers interconnected by redundant patterns. To exploit these regularities, we introduce network transformations: given a reachability formula and a network, we transform the network into a simpler to verify network and a corresponding transformed formula, such that the original formula is valid in the network if and only if the transformed formula is valid in the transformed network. Our network transformations exploit network surgery (in which irrelevant or redundant sets of nodes, headers, ports, or rules are ``sliced'' away) and network symmetry (say between backup routers). The validity of these transformations is established using a formal theory of networks. In particular, using Van Benthem-Hennessy-Milner style bisimulation, we show that one can generally associate bisimulations to transformations connecting networks and formulas with their transforms. Our work is a development in an area of current wide interest: applying programming language techniques (in our case bisimulation and modal logic) to problems in switching networks. We provide experimental evidence that our network transformations can speed up by 65x the task of verifying the communication between all pairs of Virtual Machines in a large datacenter network with about 100,000 VMs. An all-pair reachability calculation, which formerly took 5.5 days, can be done in 2 hours, and can be easily parallelized to complete in
Preceptorship versus Clinical Teaching Partnership: Literature Review and Recommendations for Implementation in Ghana
Authors: Atakro Confidence Alorse , Gross Janet
Published: April 2016

Clinical education is an essential component of the education of nursing students. However clinical nursing education in Ghana is currently facing challenges of poor working relations between hospitals and health training institutions, inadequate preceptor preparations, and inadequate faculty supervisions. Although the dominant clinical education model used in Ghana is the preceptorship model, health service and education industries are faced with challenges of lack of qualified staff, inadequately prepared preceptors, and inadequate supervision from faculty. These challenges undermine the effectiveness of the clinical learning environment and the use of the preceptorship model. The purpose of this paper was to review preceptorship and clinical teaching partnership (CTP) and make recommendations for improving clinical nursing education in Ghana. A literature review was undertaken through a search of databases that included Google Scholar, EBSCOhost, CINAHL, and HINARI. A literature review identified advantages for using clinical teaching partnership (CTP) in clinical nursing education in Ghana. Recommendations were made for the use of CTP in Ghana.
ELDP: Extended Link Duration Prediction Model for Vehicular Networks
Authors: Wang Xiufeng , Wang Chunmeng , Cui Gang , Yang Qing , Zhang Xuehai
Published: April 2016

Link duration between two vehicles is considered an important quality of service metric in designing a network protocol for vehicular networks. There exist many works that study the probability density functions of link duration in a vehicular network given various vehicle mobility models, for example, the random waypoint model. None of them, however, provides a practical solution to estimating the link duration between two vehicles on the road. This is in part because link duration between vehicles is affected by many factors including the distance between vehicles, their turning directions at intersections, and the impact of traffic lights. Considering these factors, we propose the extended link duration prediction (ELDP) model which allows a vehicle to accurately estimate how long it will be connected to another vehicle. The ELDP model does not assume that vehicles follow certain mobility models; instead, it assumes that a vehicle's velocity follows the Normal distribution. We validate the ELDP model in both highway and city scenarios in simulations. Our detailed simulations illustrate that relative speed between vehicles plays a vital role in accurately predicting link duration in a vehicular network. On the other hand, we find that the turning directions of a vehicle at intersections have subtle impact on the prediction results.
A Case of Atrial Tachycardia Circulating around a Left Atrial Roof Scar with Diabetes Mellitus and Renal Failure on Hemodialysis
Authors: Hijioka Naoko , Kamioka Masashi , Suzuki Hitoshi , Takeishi Yasuchika
Published: April 2016

Introduction. Little is known about the effects of volume change by hemodialysis (HD) and mechanical stress caused by an anatomical structure being in contact with the left atrium on the progression of atrial remodeling. We experienced a case of atrial tachycardia (AT) in a patient who had left atrial (LA) scarring at the LA roof and a low-voltage area with slow conduction around the LA scar as components of AT circuit. Here, we present the conceivable hypothesis of the LA scar and the low-voltage area formation. Our concept can be useful in developing a strategy for ablation in a patient with chronic renal failure (CRF) on HD.Case Report. A 65-year-old man with CRF on HD was referred for AT ablation. Three-dimensional electroanatomical mapping revealed that the AT conducted around an LA scar in a counterclockwise fashion. There was a slow conduction area at the superior side of the LA scar, where the AT was terminated during the ablation. Computed tomography indicated a close relationship between the LA and the anatomical structures (ascending aorta and pulmonary artery).Conclusion. Volume change by HD and close contact of anatomical structures to the LA can promote atrial remodeling, resulting in AT occurrence.
Design of Wide-Band Bandpass Filter Using Composite Right/Left-Handed Transmission Line Structure
Authors: Ren Baoping , Liu Haiwen , Guan Xuehui , Wen Pin , Xiao Xiang , Ma Zhewang
Published: April 2016

A wide-band microstrip bandpass filter (BPF) based on the improved composite right/left-handed transmission line (CRLH-TL) structure is presented in this paper. Compared to the traditional CRLH-TL with via hole, the improved one is an all-planar structure, which owns the advantage of fabrication and loss. The equivalent lossless LC circuit model of the proposed structure is established. EM software Sonnet is adopted to design the wide-band filter with bandwidth of 1.4 GHz (from 1.9 GHz to 3.3 GHz). The circuit occupies only 20.6 × 12.8 mm2. Finally, the fabrication and measurement are implemented. A good agreement between simulation and measured results verifies the validity of the design methodology.
Exact Optimum Design of Segmented Thermoelectric Generators
Authors: Zare M. , Ramin H. , Naemi S. , Hosseini R.
Published: April 2016

A considerable difference between experimental and theoretical results has been observed in the studies of segmented thermoelectric generators (STEGs). Because of simplicity, the approximate methods are widely used for design and optimization of the STEGs. This study is focused on employment of exact method for design and optimization of STEGs and comparison of exact and approximate results. Thus, using new highly efficient thermoelectric materials, four STEGs are proposed to operate in the temperature range of 300 to 1300 kelvins. The proposed STEGs are optimally designed to achieve maximum efficiency. Design and performance characteristics of the optimized generators including maximum conversion efficiency and length of elements are calculated through both exact and approximate methods. The comparison indicates that the approximate method can cause a difference up to 20% in calculation of some design characteristics despite its appropriate results in efficiency calculation. The results also show that the maximum theoretical efficiency of 23.08% is achievable using the new proposed STEGs. Compatibility factor of the selected materials for the proposed STEGs is also calculated using both exact and approximate methods. The comparison indicates a negligible difference in calculation of compatibility factor, despite the considerable difference in calculation of reduced efficiency (temperature independence efficiency).
Oral Rehabilitation of an Osteopetrosis Patient with Osteomyelitis
Authors: Celakil Tamer , Dogan Merve , Rohlig Bilge Gokcen , Evlioglu Gulumser , Keskin Haluk
Published: April 2016

Osteopetrosis is a congenital disorder characterized by increasing osteoclastic function resulting in osteomyelitis in the jaws. Orofacial findings in osteopetrosis patients are unerupted, malformed, or delayed teeth and many dental caries due to vulnerable enamel and dentin and osteomyelitis. Many reports have described that maxilla is an uncommon site of occurrence for osteomyelitis due to cortical bone morphology and collateral circulation. This report aims to discuss clinical features and prosthodontic management of a patient with clinical features of adult form of osteopetrosis and osteomyelitis in both jaws. The patient has reported better masticatory and speech efficiency with removable dentures in maxillary and mandibular jaw and also self-esteem improvement and family interaction.
Compositional Variation of PCBs, PAHs, and OCPs at Gas Phase and Size Segregated Particle Phase during Dust Incursion from the Saharan Desert in the Northwestern Anatolian Peninsula
Authors: Kuzu S. Levent
Published: April 2016

A dust incursion occurred in Istanbul on 1 February 2015 from the Saharan Desert. During this episode, 938 μg·m−3of TSP concentration was observed. TSP concentration was 64 μg·m−3and 78 μg·m−3on the following two days. Particles of 3 μm were dominant during the episode; however, particles < 0.49 μm were dominant after the episode. The averages of total (gas + particle) PCB, PAH, and OCP concentrations were 279 pg·m−3, 175 ng·m−3, and 589 pg·m−3, respectively. Tri-CBs were dominant in most of the samples. Flt and Phe had the highest contribution to PAH species.β-HCH and heptachlor had the highest share in terms of OCPs. Particle phase PCBs exhibited monomodal size distribution, whereas OCPs had bimodal size distribution. PAHs exhibited either monomodal or bimodal size distribution on different days. The mass median diameter of PAHs did not change significantly during different atmospheric conditions due to their local sources. Gas/particle partitioning of each pollutant was evaluated by plotting their subcooled vapor pressure against the partitioning coefficient. From 1 to 3 February, the slope of the regression line shifted close to −1, indicating that the least favorable conditions were present during dust incursion for an equilibrium state.
Numerical Solution of the Blasius Viscous Flow Problem by Quartic B-Spline Method
Authors: Aminikhah Hossein , Kazemi Somayyeh
Published: April 2016

A numerical method is proposed to study the laminar boundary layer about a flat plate in a uniform stream of fluid. The presented method is based on the quartic B-spline approximations with minimizing the error L2-norm. Theoretical considerations are discussed. The computed results are compared with some numerical results to show the efficiency of the proposed approach.
Quantitative EEG and Cognitive Decline in Parkinson’s Disease
Authors: Cozac Vitalii V. , Gschwandtner Ute , Hatz Florian , Hardmeier Martin , Rüegg Stephan , Fuhr Peter
Published: April 2016

Cognitive decline is common with the progression of Parkinson’s disease (PD). Different candidate biomarkers are currently studied for the risk of dementia in PD. Several studies have shown that quantitative EEG (QEEG) is a promising predictor of PD-related cognitive decline. In this paper we briefly outline the basics of QEEG analysis and analyze the recent publications addressing the predictive value of QEEG in the context of cognitive decline in PD. The MEDLINE database was searched for relevant publications from January 01, 2005, to March 02, 2015. Twenty-four studies reported QEEG findings in various cognitive states in PD. Spectral and connectivity markers of QEEG could help to discriminate between PD patients with different level of cognitive decline. QEEG variables correlate with tools for cognitive assessment over time and are associated with significant hazard ratios to predict PD-related dementia. QEEG analysis shows high test-retest reliability and avoids learning effects associated with some neuropsychological testing; it is noninvasive and relatively easy to repeat.
Sleep Quality, Sleep EEG Pattern, Mental Well-Being and Cortisol Secretion in Patients with Ruptured Aneurysm Post-Treatment: A Comparison with Post-Surgery Meningioma Patients and Controls
Authors: Gerber Markus , Colledge Flora , Pühse Uwe , Holsboer-Trachsler Edith , Zimmerer Stefan , Brand Serge
Published: April 2016

Background: Although the chance of surviving an aneurysmal subarachnoid haemorrhage (aSAH) has increased steadily, disturbed sleep and persistent psychological complaints are frequently experienced post-ictus. To date, however, few studies have sought to determine whether physiological parameters, such as objectively measured sleep and cortisol secretion, interrelate significantly with low sleep quality and psychological complaints such as depression. Furthermore, there is little evidence as to whether post-ictal complaints differ between aSAH patients and other groups who have experienced stressful medical intervention. Methods: Data on objective and subjective sleep, sleep-related dysfunctional cognitions, psychological functioning and cortisol secretion were collected from 15 patients who had undergone medical intervention for aSAH. Data were also collected from a group of 16 individuals who had undergone surgery for a meningioma and a third group made up of 17 healthy participants. Results: aSAH patients and meningioma patients had significantly poorer subjective sleep than healthy controls and reported more sleep-related dysfunctional cognitions and hypochondriacal beliefs. They also had a significantly higher morning cortisol response. Finally, a non-significant trend was found showing that aSAH patients and meningioma patients reported poorer psychological functioning than healthy controls. Conclusion: Following treatment, aSAH patients and meningioma patients experience poorer subjective sleep and some differences in objectively measured sleep, which might be attributable to increased sleep-related dysfunctional cognitions and poorer overall psychological functioning. Differences in cortisol production were also observed, suggesting that some physiological imbalances are still present post-ictus.