bluuebunny/crossref_metadata_2025 huggingface dataset:
Exploring Uncertainty with Projectile Launchers
Authors: Orzel Chad , Reich Gary , Marr Jonathan
Published: November 2012

The proper choice of a measurement technique that minimizes systematic and random uncertainty is an essential part of experimental physics. These issues are difficult to teach in the introductory laboratory, though. Because most experiments involve only a single measurement technique, students are often unable to make a clear distinction between random and systematic uncertainties, or to compare the uncertainties associated with different techniques. In this paper, we describe an experiment suitable for an introductory college-level (or advanced high school) course that uses velocity measurements to clearly show students the effects of both random and systematic uncertainties.
Sequential Conformational Rearrangements Dictate the Dynamics of Class C GPCR Activation
Authors: Lane J. Robert , Canals Meritxell
Published: November 2012

Fluorescent probes reveal the roles of domain rearrangement and dimerization in GPCR activation.
Science Signaling
Podcast: 20 November 2012
Authors: Lefkowitz Robert J. , VanHook Annalisa M.
Published: November 2012

The 2012 Nobel Prize in Chemistry honors research on the function of G protein–coupled receptors.
Tumorigenic Targets of IKKε
Authors: Gough Nancy R.
Published: November 2012

The kinase IKKε promotes oncogenic signaling by phosphorylating the adaptor TRAF2.
Intensification of Antiretroviral Therapy through Addition of Enfuvirtide in Naive HIV-1-Infected Patients with Severe Immunosuppression Does Not Improve Immunological Response: Results of a Randomized Multicenter Trial (ANRS 130 Apollo)
Authors: Joly Véronique , Fagard Catherine , Grondin Carine , Descamps Diane , Yazdanpanah Yazdan , Charpentier Charlotte , Colin de Verdiere Nathalie , Tabuteau Sophie , Raffi François , Cabie André , Chene Geneviève , Yeni Patrick ,   the ANRS 130 Apollo Trial Group
Published: November 2012

We studied whether addition of enfuvirtide (ENF) to a background combination antiretroviral therapy (cART) would improve the CD4 cell count response at week 24 in naive patients with advanced HIV disease. ANRS 130 Apollo is a randomized study, conducted in naive HIV-1-infected patients, either asymptomatic with CD4 counts of <100/mm3or stage B/C disease with CD4 counts of <200/mm3. Patients received tenofovir-emtricitabine with lopinavir-ritonavir (LPV/r) or efavirenz and were randomized to receive ENF for 24 weeks (ENF arm) or not (control arm). The primary endpoint was the proportion of patients with CD4 counts of ≥200/mm3at week 24. A total of 195 patients were randomized: 73% had stage C disease, 78% were male, the mean age was 44 years, the median CD4 count was 30/mm3, and the median HIV-1 RNA load was 5.4 log10copies/ml. Eighty-one percent of patients received LPV/r. One patient was lost to follow-up, and eight discontinued the study (four in each arm). The proportions of patients with CD4 counts of ≥200/mm3at week 24 were 34% and 38% in the ENF and control arms, respectively (P= 0.53). The proportions of patients with HIV-1 RNA loads of <50 copies/ml were 74% and 58% at week 24 in the ENF and control arms, respectively (P< 0.02), and the proportion reached 79% in both arms at week 48. Twenty (20%) and 12 patients (13%) in the ENF and control arms, respectively, experienced at least one AIDS event during follow-up (P= 0.17). Although inducing a more rapid virological response, addition of ENF to a standard cART does not improve the immunological outcome in naive HIV-infected patients with severe immunosuppression.
In Vitro
Activity of Calcineurin and Heat Shock Protein 90 Inhibitors against Aspergillus fumigatus Azole- and Echinocandin-Resistant Strains
Authors: Lamoth Frédéric , Juvvadi Praveen R. , Gehrke Christopher , Steinbach William J.
Published: November 2012

Due to the limited number of antifungals and the emergence of resistance, new therapies against invasive aspergillosis are needed. We show that calcineurin inhibitors are active
in vitro
against both azole- and echinocandin-resistant
Aspergillus fumigatus
strains. The heat shock protein 90 (Hsp90) inhibitor geldanamycin had modest activity when used alone, but its combination with caspofungin or tacrolimus (FK506) resulted in fungicidal activity against azole-resistant strains. Targeting the Hsp90-calcineurin axis is a promising alternative strategy against azole-resistant
A. fumigatus
strains.
Vaccination coverage and out-of-sequence vaccinations in rural Guinea-Bissau: an observational cohort study
Authors: Hornshøj Linda , Benn Christine Stabell , Fernandes Manuel , Rodrigues Amabelia , Aaby Peter , Fisker Ane Bærent
Published: November 2012

Objective

The WHO aims for 90% coverage of the Expanded Program on Immunization (EPI), which in Guinea-Bissau included BCG vaccine at birth, three doses of diphtheria−tetanus−pertussis vaccine (DTP) and oral polio vaccine (OPV) at 6, 10 and 14 weeks and measles vaccine (MV) at 9 months when this study was conducted. The WHO assesses coverage by 12 months of age. The sequence of vaccines may have an effect on child mortality, but is not considered in official statistics or assessments of programme performance. We assessed vaccination coverage and frequency of out-of-sequence vaccinations by 12 and 24 months of age.

Design

Observational cohort study.

Setting and participants

The Bandim Health Project's (BHP) rural Health and Demographic Surveillance site covers 258 randomly selected villages in all regions of Guinea-Bissau. Villages are visited biannually and vaccination cards inspected to ascertain vaccination status. Between 2003 and 2009 vaccination status by 12 months of age was assessed for 5806 children aged 12–23 months; vaccination status by 24 months of age was assessed for 3792 children aged 24–35 months.

Outcome measures

Coverage of EPI vaccinations and frequency of out-of-sequence vaccinations.

Results

Half of 12-month-old children and 65% of 24-month-old children had completed all EPI vaccinations. Many children received vaccines out of sequence: by 12 months of age 54% of BCG-vaccinated children had received DTP with or before BCG and 28% of measles-vaccinated children had received DTP with or after MV. By 24 months of age the proportion of out-of-sequence vaccinations was 58% and 35%, respectively, for BCG and MV.

Conclusions

In rural Guinea-Bissau vaccination coverage by 12 months of age was low, but continued to increase beyond 12 months of age. More than half of all children received vaccinations out of sequence. This highlights the need to improve vaccination services.
Childhood motocross truncal injuries: high-velocity, focal force to the chest and abdomen
Authors: Kennedy Raelene D , Potter D Dean , Osborn John B , Zietlow Scott , Zarroug Abdalla E , Moir Christopher R , Ishitani Michael B , McIntosh Amy
Published: November 2012

Objectives

To review the need for operative intervention and critical care services for motocross truncal injuries in children.

Design cohort

Retrospective review of patients identified via the hospital trauma registry.

Setting

Our Level 1 Pediatric Trauma Center serves five motocross tracks. These patients require frequent medical care for injuries.

Participants

All patients ≤17 years of age with truncal injuries sustained during motocross activities, between 2000 and 2011, were identified through the trauma registry.

Primary and secondary outcome measures

Operative intervention, intensive care unit (ICU) admission, length of stay, morbidity and demographics were reviewed.

Results

Motocross injured 162 children. Thirty (18.5%) were thoracic or abdominal injuries. Operative intervention was required in eight (27%) patients. Mean injury severity score (ISS) was 11.8. ICU admission was required in 50% and average hospital length of stay was 4.1 days. The most common injuries include pulmonary contusion, pneumothorax, spleen and liver lacerations. 13% of subjects suffered truncal injury from motocross on more than one occasion.

Conclusions

Paediatric motocross-related truncal injuries are significant. Surgical intervention is required in 27% of patients. The lower ISS incurred from motocross combined with high surgical and ICU admission rates suggests focal high-impact injuries to the chest and abdomen. Despite significant injury, 13% of motocross patients suffer recurrent injuries. Parents and children need injury prevention education.
Spline-based modelling of trends in the force of HIV infection, with application to the UNAIDS Estimation and Projection Package
Authors: Hogan Daniel R , Salomon Joshua A
Published: November 2012

Objective

We previously developed a flexible specification of the UNAIDS Estimation and Projection Package (EPP) that relied on splines to generate time-varying values for the force of infection parameter. Here, we test the feasibility of this approach for concentrated HIV/AIDS epidemics with very sparse data and compare two methods for making short-term future projections with the spline-based model.

Methods

Penalised B-splines are used to model the average infection risk over time within the EPP 2011 modelling framework, which includes antiretroviral treatment effects and CD4 cell count progression, and is fit to sentinel surveillance prevalence data with a Bayesian algorithm. We compare two approaches for future projections: (1) an informative prior related to equilibrium prevalence and (2) a random walk formulation.

Results

The spline-based model produced plausible fits across a range of epidemics, which included 87 subpopulations from 14 countries with concentrated epidemics and 75 subpopulations from 33 countries with generalised epidemics. The equilibrium prior and random walk approaches to future projections yielded similar prevalence estimates, and both performed well in tests of out-of-sample predictive validity for prevalence. In contrast, in some cases the two approaches varied substantially in estimates of incidence, with the random walk formulation avoiding extreme changes in incidence.

Conclusions

A spline-based approach to allowing the force of infection parameter to vary over time within EPP 2011 is robust across a diverse array of epidemics, including concentrated ones with limited surveillance data. Future work on the EPP model should consider the impact that different modelling approaches have on estimates of HIV incidence.
Effect of Ferroelectric Polarization on Carrier Transport in Controlled Polarization-Type Ferroelectric Gate Field-Effect Transistors with Poly(vinylidene fluoride–tetrafluoroethylene)/ZnO Heterostructure
Authors: Yamada Hiroaki , Yoshimura Takeshi , Fujimura Norifumi
Published: November 2012

The carrier transport properties of ferroelectric gate field-effect transistors composed of oxide polar semiconductors, ZnO, and organic ferroelectrics, poly(vinylidene fluoride–tetrafluoroethylene) [P(VDF–TeFE)], were investigated. The P(VDF–TeFE)/ZnO heterostructure with a 100-nm-thick channel shows a large ON/OFF ratio of 105 in the drain current while that with a channel thickness of 500 nm shows small changes. To clarify the effect of ferroelectric polarization on the carrier transport properties, Hall effect measurement was carried out after poling treatment. Although the Hall mobility for the channel thickness of 500 nm shows no dependence on the poling voltage, that for the channel thickness of 100 nm increases with increasing poling voltage. The temperature dependence of the carrier transport properties indicates that the Hall mobility for the channel thickness of 100 nm increases when the carriers are accumulated at the interface between P(VDF–TeFE) and ZnO, especially below 200 K. The results suggest that the reduction in ionized impurity scattering, which originates from the carrier accumulation due to ferroelectric polarization, increases the mobility.
Nonvolatile Power-Gating Field-Programmable Gate Array Using Nonvolatile Static Random Access Memory and Nonvolatile Flip-Flops Based on Pseudo-Spin-Transistor Architecture with Spin-Transfer-Torque Magnetic Tunnel Junctions
Authors: Yamamoto Shuu'ichirou , Shuto Yusuke , Sugahara Satoshi
Published: November 2012

We proposed and computationally analyzed a nonvolatile power-gating field-programmable gate array (NVPG-FPGA) based on pseudo-spin-transistor architecture with spin-transfer-torque magnetic tunnel junctions (STT-MTJs). The circuit employs nonvolatile static random memory (NV-SRAM) cells and nonvolatile flip-flops (NV-FFs) as the storage circuits of the NVPG-FPGA. The circuit configuration and microarchitecture are compatible with SRAM-based FPGAs, and the additional nonvolatile memory functionality makes it possible to execute efficient power gating (PG). The break-even time (BET) for the nonvolatile configuration logic block (NV-CLB) of the NVPG-FPGA was also analyzed, and reduction techniques of the BET, which allows highly efficient PG operations with fine granularity, were proposed.
Phonon-Kick Mechanism for Defect Reactions in Semiconductors
Authors: Shinozuka Yuzo , Wakita Masaki , Suzuki Kei
Published: November 2012

The possibility of a feedback mechanism between nonradiative carrier captures by a deep-level defect and induced transient lattice vibrations is discussed using appropriate configuration coordinate diagrams for many carriers. By treating the lattice motion classically, we self-consistently simulate the time evolution of the interaction mode and a series of athermal captures of electron(s) and hole(s). When both the activation energies E
e
act and E
h
act are low, a series of successive nonradiative carrier-captures are possible for high carrier densities. However, we find that the possibility of inflation in the amplitude of lattice vibration critically depends on minority carrier capture rate and the relative width of the phonon frequency distribution. Referring to the obtained results, we discuss the phonon-kick mechanism for defect reactions.
Nanoimprinted Step-Edge Vertical-Channel Organic Transistors
Authors: Kudo Kazuhiro , Yamauchi Hiroshi , Sakai Masatoshi
Published: November 2012

Flexible and low-cost organic field-effect transistors (OFETs) are desired for a variety of organic electronics. In this paper, we describe step-edge vertical-channel OFETs (SVC-OFETs) having excellent device performance fabricated by nanoimprint lithography and a self-aligned process. SVC-OFETs can be used to fabricate a submicron channel by forming the channel region around the step edge. The carriers flow in the vertical direction in the short channel along the step-edge structure. Both n- and p-channel FETs are also realized by a solution process.
Porous to Nonporous Transition in the Morphology of Metal Assisted Etched Silicon Nanowires
Authors: Lotty Olan , Petkov Nikolay , Georgiev Yordan M. , Holmes Justin D.
Published: November 2012

A single step metal assisted etching (MAE) process, utilizing metal ion-containing HF solutions in the absence of an external oxidant, has been developed to generate heterostructured Si nanowires with controllable porous (isotropically etched) and non-porous (anisotropically etched) segments. Detailed characterisation of both the porous and non-porous sections of the Si nanowires was provided by transmission electron microscopy studies, enabling the mechanism of nanowire roughening to be ascertained. The versatility of the MAE method for producing heterostructured Si nanowires with varied and controllable textures is discussed in detail.
Numerical Approach to the Investigation of Performance of Silicon Nanowire Solar Cells Embedded in a SiO2 Matrix
Authors: Kurokawa Yasuyoshi , Kato Shinya , Watanabe Yuya , Yamada Akira , Konagai Makoto , Ohta Yoshimi , Niwa Yusuke , Hirota Masaki
Published: November 2012

The electrical characteristics of silicon nanowire (SiNW) solar cells with p-type hydrogenated amorphous silicon oxide (E
g = 1.9 eV)/n-type SiNWs embedded in a SiO2/n-type hydrogenated amorphous silicon oxide (E
g = 1.9 eV) structure have been investigated using two- and three-dimensional device simulators, taking into account the quantum size effect. The average bandgap of a SiNW embedded in SiO2 increased from 1.15 to 2.68 eV with decreasing diameter from 10 to 2 nm, owing to the quantum size effect. Note that under sunlight of AM1.5G, the open-circuit voltage (V
oc) of SiNW solar cells also increased to 1.46 V with decreasing diameter of the SiNWs to 2 nm. This result suggests that it is possible to enhance V
oc by applying the quantum size effect, and a SiNW is a promising material for all-silicon tandem solar cells.
Layer-by-Layer Assembled Transparent Conductive Graphene Films for Silicon Thin-Film Solar Cells
Authors: Ishikawa Ryousuke , Bando Masashi , Wada Hidetoshi , Kurokawa Yasuyoshi , Sandhu Adarsh , Konagai Makoto
Published: November 2012

The potential of chemically derived graphene as a solution-processable transparent conductive film has been explored. Synthesis of amine-functionalized graphene oxide was intended for its utilization in layer-by-layer (LBL) assembly. LBL assembly of graphene oxide was utilized to fabricate graphene-based thin films in a scalable and highly reproducible way. It was found that the optical transmittance and sheet resistance of the film decrease with an increase in the number of LBL cycles in a reproducible way. The sheet resistance of the LBL-assembled GO film was improved by an order of magnitude at the same optical transparency due to the good uniformity and stacking of graphene flakes. Furthermore, we demonstrated the potential for the window electrodes of silicon thin-film solar cells.
Formation of ZnO Nanoparticles by ZnO- and O- Dual Beam Ion Implantation and Thermal Annealing
Authors: Pandey Bimal , Poudel Prakash R. , Weathers Duncan L.
Published: November 2012

ZnO nanoparticles have been synthesized by dual beam ion implantation into Si. 45 keV ZnO- molecular ions and 15 keV O- ions were implanted into Si at room temperature to fluences of 1 ×1017 and 2 ×1017 ions/cm2, respectively. In the as-implanted sample, Zn nanoparticles with average crystalline size of ∼4.5 nm were observed to have formed and were distributed from the sample surface to a depth of ∼76 nm. The implanted sample was thermally annealed at a temperature of 700 °C in a mixture of Ar and H2 for 1 h, after which both the Zn and O spatial distributions were observed to have broadened and ZnO nanoparticles with average crystalline size of ∼17.5 nm were formed. Due to the O- ion implantation, a thickness of ∼38 nm of Si wafer was transformed into SiO2, and the SiO2 layer thickened to ∼57 nm when the sample was annealed. Binding energies of Zn increased in the annealed sample as compared to the as-implanted sample for all measured depths, consistent with the formation of ZnO bonding and indicating that ZnO had formed throughout the SiO2 layer and slightly beyond.
Evidence of Kinetically Stable Glassy Phase Formation in Ultrathin NdNiO3 Films
Authors: Prestgard Megan Campbell , Tiwari Ashutosh
Published: November 2012

We are reporting the time and temperature dependence of the electrical resistivity exhibited by ultrathin NdNiO3 films. Films with thicknesses ranging from 0.6 to 120 nm were grown on single crystal LaAlO3 substrate (001) using a pulsed laser deposition technique. Temperature dependence of the electrical resistivity indicated dissipation of strain effects for thicknesses ranging from 0.6 to 6 nm, below the critical thickness for defect formation, approximately 12 nm. Strain dissipation prior to defect formation occurred due to a decrease in the Ni–O–Ni bond angle with increasing film thickness resulting from an increased freedom of movement in the NiO6 octahedra. Subsequent defect formation and clustering in the 60 and 120 nm samples resulted in a domination of the material properties by defects rather than strain effects. Our study showed that below the metal–insulator transition temperature, electrical resistivity of the films was very strongly time dependent. A plausible mechanism of kinetically stable glassy phase formation has been proposed which not only explains the time dependence of the electrical resistivity data but also accounts for its anomalous temperature dependence at low temperatures.
Inhomogeneous Microstructure and Electrical Transport Properties at the LaAlO3/SrTiO3 Interface
Authors: Kalabukhov Alexey , Claeson Tord , Aurino Pier Paolo , Gunnarsson Robert , Winkler Dag , Olsson Eva , Tuzla Nikolina , Börjesson Johan , Cao Yu , Nyborg Lars , Boikov Yuri A. , Serenkov Igor T. , Sakharov Vladimir I. , Volkov Mikhail P.
Published: November 2012

Medium-energy ion spectroscopy (MEIS), scanning transmission electron microscopy (STEM) and X-ray photoemission spectroscopy (XPS) were used to investigate the composition and microstructure of LaAlO3/SrTiO3 (LAO/STO) interfaces grown by pulsed laser deposition of LAO on TiO2-terminated STO substrates under different oxidizing conditions. MEIS and XPS indicated Sr/La and Al/Ti intermixing within several atomic layers at all studied interfaces. XPS and STEM revealed that La diffuses deeper than Al. Analysis of the MEIS data suggests inhomogeneous lateral distribution of the diffused elements. This is further supported by the observation of a large positive magneto-resistance at low temperatures. We discuss the role of lateral inhomogeneities on the formation of the electron gas at the LAO/STO interface.
Epitaxial Structures of Band-Gap-Engineered α-(CrxFe1-x)2O3 (0 ≤x≤1) Films Grown on C-Plane Sapphire
Authors: Mashiko Hisanori , Oshima Takayoshi , Ohtomo Akira
Published: November 2012

Solid solutions of α-Cr2O3 and α-Fe2O3 are novel oxide semiconductors exhibiting narrower band gaps than those of the end members. We have investigated the heteroepitaxial growth and crystalline structure of pulsed-laser deposited α-(Cr
x
Fe1-x
)2O3 films on c-plane sapphire substrates. Under the growth condition optimized for α-Fe2O3, reflection high-energy electron diffraction intensity oscillations were observable for both α-Fe2O3 and α-Cr2O3, enabling us to control film thickness in a layer-by-layer fashion. The composition dependence of the epitaxial structures, including phase purity, orientation, strain, and in-plane rotation domain, was characterized by X-ray diffraction to reveal a defect-free composition range (0 ≤x ≤0.50). The films with 0.60 ≤x ≤1 were found to have 180°-rotation domains. The absorption spectra of α-(Cr0.50Fe0.50)2O3 solid solution (corundum) and superlattice (nominally composed ilmenite) films are compared with those of end members and an α-Fe2O3/α-Cr2O3 bilayer film to elucidate the origin of the band-gap narrowing.
Atomic Scale Imaging of TiO2(100) Reconstructed Surfaces by Noncontact Scanning Nonlinear Dielectric Microscopy
Authors: Sawai Nobuhiro , Yamasue Kohei , Cho Yasuo
Published: November 2012

We performed noncontact scanning nonlinear dielectric microscopy (NC-SNDM) measurements to investigate both the topography and polarization distribution images of a reconstructed TiO2(100) surface. To acquire an atomic resolution image of the (110) surface, which is the most stable in TiO2, NC-SNDM requires annealing at a temperature higher than that for scanning tunneling microscopy (STM). However, in the case of the (100) surface, we found that annealing at the same temperature as that used for STM was sufficient. The two types of reconstructed surfaces were measured using NC-SNDM. We confirmed we could even achieve NC-SNDM measurements in a dielectric material by reducing the thickness of the specimen and making the specimen nonstoichiometric without any annealing. These results show that NC-SNDM has superb capabilities that STM does not have, including the capability to measure the topography and polarization distribution even in a dielectric material, by inducing polarization near the surface without any means of inducing conductivity.
Iterative Frequency Domain Decision Feedback Equalization and Decoding for Underwater Acoustic Communications
Authors: Zhao Liang , Ge Jian-Hua
Published: November 2012

Single-carrier (SC) transmission with frequency-domain equalization (FDE) is today recognized as an attractive alternative to orthogonal frequency-division multiplexing (OFDM) for communication application with the inter-symbol interference (ISI) caused by multi-path propagation, especially in shallow water channel. In this paper, we investigate an iterative receiver based on minimum mean square error (MMSE) decision feedback equalizer (DFE) with symbol rate and fractional rate samplings in the frequency domain (FD) and serially concatenated trellis coded modulation (SCTCM) decoder. Based on sound speed profiles (SSP) measured in the lake and finite-element ray tracking (Bellhop) method, the shallow water channel is constructed to evaluate the performance of the proposed iterative receiver. Performance results show that the proposed iterative receiver can significantly improve the performance and obtain better data transmission than FD linear and adaptive decision feedback equalizers, especially in adopting fractional rate sampling.
Data assimilation using sequential monte carlo methods in wildfire spread simulation
Authors: Xue Haidong , Gu Feng , Hu Xiaolin
Published: November 2012

Assimilating real-time sensor data into large-scale spatial-temporal simulations, such as simulations of wildfires, is a promising technique for improving simulation results. This asks for advanced data assimilation methods that can work with the complex structures and nonlinear behaviors associated with the simulation models. This article presents a data assimilation framework using Sequential Monte Carlo (SMC) methods for wildfire spread simulations. The models and algorithms of the framework are described, and experimental results are provided. This work demonstrates the feasibility of applying SMC methods to data assimilation of wildfire spread simulations. The developed framework can potentially be generalized to other application areas where sophisticated simulation models are used.
Formal verification of monad transformers
Authors: Huffman Brian
Published: November 2012

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses.

We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.
Functional programming with structured graphs
Authors: Oliveira Bruno C.d.S. , Cook William R.
Published: November 2012

This paper presents a new functional programming model for graph structures called
structured graphs
. Structured graphs extend conventional algebraic datatypes with explicit definition and manipulation of cycles and/or sharing, and offer a practical and convenient way to program graphs in functional programming languages like Haskell. The representation of sharing and cycles (edges) employs recursive binders and uses an encoding inspired by
parametric higher-order abstract syntax
. Unlike traditional approaches based on mutable references or node/edge lists,
well-formedness
of the graph structure is ensured statically and reasoning can be done with standard functional programming techniques. Since the binding structure is generic, we can define many useful generic combinators for manipulating structured graphs. We give applications and show how to reason about structured graphs.
Operational semantics using the partiality monad
Authors: Danielsson Nils Anders
Published: November 2012

The operational semantics of a partial, functional language is often given as a relation rather than as a function. The latter approach is arguably more natural: if the language is functional, why not take advantage of this when defining the semantics? One can immediately see that a functional semantics is deterministic and, in a constructive setting, computable.

This paper shows how one can use the coinductive partiality monad to define big-step or small-step operational semantics for lambda-calculi and virtual machines as total, computable functions (total definitional interpreters). To demonstrate that the resulting semantics are useful type soundness and compiler correctness results are also proved. The results have been implemented and checked using Agda, a dependently typed programming language and proof assistant.
Equality proofs and deferred type errors
Authors: Vytiniotis Dimitrios , Peyton Jones Simon , Magalhães José Pedro
Published: November 2012

The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates first-class equality proofs in its intermediate language. We describe a simple, elegant technique that exploits these equality proofs to support deferred type errors. The technique requires us to treat equality proofs as possibly-divergent terms; we show how to do so without losing either soundness or the zero-overhead cost model that the programmer expects.
Work efficient higher-order vectorisation
Authors: Lippmeier Ben , Chakravarty Manuel M.T. , Keller Gabriele , Leshchinskiy Roman , Peyton Jones Simon
Published: November 2012

Existing approaches to
higher-order vectorisation
, also known as
flattening nested data parallelism
, do not preserve the asymptotic work complexity of the source program. Straightforward examples, such as sparse matrix-vector multiplication, can suffer a severe blow-up in both time and space, which limits the practicality of this method. We discuss why this problem arises, identify the mis-handling of index space transforms as the root cause, and present a solution using a refined representation of nested arrays. We have implemented this solution in Data Parallel Haskell (DPH) and present benchmarks showing that realistic programs, which used to suffer the blow-up, now have the correct asymptotic work complexity. In some cases, the asymptotic complexity of the vectorised program is even better than the original.
Propositions as sessions
Authors: Wadler Philip
Published: November 2012

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.
A generic abstract syntax model for embedded languages
Authors: Axelsson Emil
Published: November 2012

Representing a syntax tree using a data type often involves having many similar-looking constructors. Functions operating on such types often end up having many similar-looking cases. Different languages often make use of similar-looking constructions. We propose a generic model of abstract syntax trees capable of representing a wide range of typed languages. Syntactic constructs can be composed in a modular fashion enabling reuse of abstract syntax and syntactic processing within and across languages. Building on previous methods of encoding extensible data types in Haskell, our model is a pragmatic solution to Wadler's "expression problem". Its practicality has been confirmed by its use in the implementation of the embedded language Feldspar.
Introspective pushdown analysis of higher-order programs
Authors: Earl Christopher , Sergey Ilya , Might Matthew , Van Horn David
Published: November 2012

In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. This work illuminates and conquers the theoretical challenges that stand in the way of combining the power of these techniques. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access during transition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does.
Introspective
pushdown systems resolve this conflict. Introspective pushdown systems provide enough access to the stack to allow abstract garbage collection, but they remain restricted enough to compute control-state reachability, thereby enabling the sound and precise product of pushdown analysis and abstract garbage collection. Experiments reveal synergistic interplay between the techniques, and the fusion demonstrates "better-than-both-worlds" precision.
Safe compiler-driven transaction checkpointing and recovery
Authors: Sreeram Jaswanth , Pande Santosh
Published: November 2012

Several studies have shown that a large fraction of the work performed inside memory transactions in representative programs is wasted due to the transaction experiencing a conflict and aborting. Aborts inside long running transactions are especially influential to performance and the simplicity of the TM programming model (relative to using finegrained locking) in synchronizing large critical sections means that large transactions are common and this exacerbates the problem of wasted work. In this paper we present a practical transaction checkpoint and recovery scheme in which transactions that experience a conflict can restore their state (including the local context in which they were executing) to some dynamic program point before this access and begin execution from that point. This state saving and restoration is implemented by checkpoint operations that are generated by a compiler into the transaction's body and are also optimized to reduce the amount of state that is saved and restored. We also describe a runtime system that manages these checkpointed states and orchestrates the restoration of the right checkpointed state for a conflict on a particular transactional access. Moreover the synthesis of these save and restore operations, their optimization and invocation at runtime are completely transparent to the programmer. We have implemented the checkpoint generation and optimization scheme in the LLVM compiler and runtime support for the TL2 STM system. Our experiments indicate that for many parallel programs using such checkpoint recovery schemes can result in upto several orders of magnitude reduction in number of aborts and significant execution time speedups relative to plain transactional programs for the same number of threads.
Towards a practical secure concurrent language
Authors: Muller Stefan , Chong Stephen
Published: November 2012

We demonstrate that a practical concurrent language can be extended in a natural way with information security mechanisms that provably enforce strong information security guarantees. We extend the X10 concurrent programming language with coarse-grained information-flow control. Central to X10 concurrency abstractions is the notion of a place: a container for data and computation. We associate a security level with each place, and restrict each place to store only data appropriate for that security level. When places interact only with other places at the same security level, then our security mechanisms impose no restrictions. When places of differing security levels interact, our information security analysis prevents potentially dangerous information flows, including information flow through covert scheduling channels. The X10 concurrency mechanisms simplify reasoning about information flow in concurrent programs. We present a static analysis that enforces a noninterference-based extensional information security condition in a calculus that captures the key aspects of X10's place abstraction and async-finish parallelism. We extend this security analysis to support many of X10's language features, and have implemented a prototype compiler for the resulting language.
Mitigating the compiler optimization phase-ordering problem using machine learning
Authors: Kulkarni Sameer , Cavazos John
Published: November 2012

Today's compilers have a plethora of optimizations to choose from, and the correct choice of optimizations can have a significant impact on the performance of the code being optimized. Furthermore, choosing the correct order in which to apply those optimizations has been a long standing problem in compilation research. Each of these optimizations interacts with the code and in turn with all other optimizations in complicated ways. Traditional compilers typically apply the same set of optimization in a fixed order to all functions in a program, without regard the code being optimized.

Understanding the interactions of optimizations is very important in determining a good solution to the phase-ordering problem. This paper develops a new approach that automatically selects good optimization orderings on a per method basis within a dynamic compiler. Our approach formulates the phase-ordering problem as a Markov process and uses a characterization of the current state of the code being optimized to creating a better solution to the phase ordering problem. Our technique uses
neuro-evolution
to construct an artificial neural network that is capable of predicting beneficial optimization ordering for a piece of code that is being optimized. We implemented our technique in Jikes RVM and achieved significant improvements on a set of standard Java benchmarks over a well-engineered fixed order.
Optimization coaching
Authors: St-Amour Vincent , Tobin-Hochstadt Sam , Felleisen Matthias
Published: November 2012

Optimizing compilers map programs in high-level languages to high-performance target language code. To most programmers, such a compiler constitutes an impenetrable black box whose inner workings are beyond their understanding. Since programmers often must understand the workings of their compilers to achieve their desired performance goals, they typically resort to various forms of reverse engineering, such as examining compiled code or intermediate forms. Instead, optimizing compilers should engage programmers in a dialog. This paper introduces one such possible form of dialog: optimization coaching. An optimization coach watches while a program is compiled, analyzes the results, generates suggestions for enabling further compiler optimization in the source program, and presents a suitable synthesis of its results to the programmer. We present an evaluation based on case studies, which illustrate how an optimization coach can help programmers achieve optimizations resulting in substantial performance improvements.
On the benefits and pitfalls of extending a statically typed language JIT compiler for dynamic scripting languages
Authors: Castanos Jose , Edelsohn David , Ishizaki Kazuaki , Nagpurkar Priya , Nakatani Toshio , Ogasawara Takeshi , Wu Peng
Published: November 2012

Whenever the need to compile a new dynamically typed language arises, an appealing option is to repurpose an existing statically typed language Just-In-Time (JIT) compiler (repurposed JIT compiler). Existing repurposed JIT compilers (RJIT compilers), however, have not yet delivered the hoped-for performance boosts. The performance of JVM languages, for instance, often lags behind standard interpreter implementations. Even more customized solutions that extend the internals of a JIT compiler for the target language compete poorly with those designed specifically for dynamically typed languages. Our own Fiorano JIT compiler is an example of this problem. As a state-of-the-art, RJIT compiler for Python, the Fiorano JIT compiler outperforms two other RJIT compilers (Unladen Swallow and Jython), but still shows a noticeable performance gap compared to PyPy, today's best performing Python JIT compiler. In this paper, we discuss techniques that have proved effective in the Fiorano JIT compiler as well as limitations of our current implementation. More importantly, this work offers the first in-depth look at benefits and limitations of the repurposed JIT compiler approach. We believe the most common pitfall of existing RJIT compilers is not focusing sufficiently on specialization, an abundant optimization opportunity unique to dynamically typed languages. Unfortunately, the lack of specialization cannot be overcome by applying traditional optimizations.
An abstract interpretation framework for refactoring with application to extract methods with contracts
Authors: Cousot Patrick M. , Cousot Radhia , Logozzo Francesco , Barnett Michael
Published: November 2012

Method extraction is a common refactoring feature provided by most modern IDEs. It replaces a user-selected piece of code with a call to an automatically generated method. We address the problem of automatically inferring contracts (precondition, postcondition) for the extracted method. We require the inferred contract: (a) to be valid for the extracted method (validity); (b) to guard the language and programmer assertions in the body of the extracted method by an opportune precondition (safety); (c) to preserve the proof of correctness of the original code when analyzing the new method separately (completeness); and (d) to be the most general possible (generality). These requirements rule out trivial solutions (e.g., inlining, projection, etc). We propose two theoretical solutions to the problem. The first one is simple and optimal. It is valid, safe, complete and general but unfortunately not effectively computable (except for unrealistic finiteness/decidability hypotheses). The second one is based on an iterative forward/backward method. We show it to be valid, safe, and, under reasonable assumptions, complete and general. We prove that the second solution subsumes the first. All justifications are provided with respect to a new, set-theoretic version of Hoare logic (hence without logic), and abstractions of Hoare logic, revisited to avoid surprisingly unsound inference rules.

We have implemented the new algorithms on the top of two industrial-strength tools (CCCheck and the Microsoft Roslyn CTP). Our experience shows that the analysis is both fast enough to be used in an interactive environment and precise enough to generate good annotations.
Automating object transformations for dynamic software updating
Authors: Magill Stephen , Hicks Michael , Subramanian Suriya , McKinley Kathryn S.
Published: November 2012

Dynamic software updating (DSU) systems eliminate costly downtime by dynamically fixing bugs and adding features to executing programs. Given a static code patch, most DSU systems construct runtime code changes automatically. However, a dynamic update must also specify how to change the running program's execution state, e.g., the stack and heap, to make it compatible with the new code. Constructing such state transformations correctly and automatically remains an open problem. This paper presents a solution called Targeted Object Synthesis (TOS). TOS first executes the same tests on the old and new program versions separately, observing the program heap state at a few corresponding points. Given two corresponding heap states, TOS matches objects in the two versions using key fields that uniquely identify objects and correlate old and new-version objects. Given example object pairs, TOS then synthesizes the simplest-possible function that transforms an old-version object to its new-version counterpart. We show that TOS is effective on updates to four open-source server programs for which it generates non-trivial transformation functions that use conditionals, operate on collections, and fix memory leaks. These transformations help programmers understand their changes and apply dynamic software updates.
Elixir
Authors: Prountzos Dimitrios , Manevich Roman , Pingali Keshav
Published: November 2012

Algorithms in new application areas like machine learning and network analysis use "irregular" data structures such as graphs, trees and sets. Writing efficient parallel code in these problem domains is very challenging because it requires the programmer to make many choices: a given problem can usually be solved by several algorithms, each algorithm may have many implementations, and the best choice of algorithm and implementation can depend not only on the characteristics of the parallel platform but also on properties of the input data such as the structure of the graph. One solution is to permit the application programmer to experiment with different algorithms and implementations without writing every variant from scratch. Auto-tuning to find the best variant is a more ambitious solution. These solutions require a system for automatically producing efficient parallel implementations from high-level specifications. Elixir, the system described in this paper, is the first step towards this ambitious goal. Application programmers write specifications that consist of an
operator
, which describes the computations to be performed, and a
schedule
for performing these computations. Elixir uses sophisticated inference techniques to produce efficient parallel code from such specifications.

We used Elixir to automatically generate many parallel implementations for three irregular problems: breadth-first search, single source shortest path, and betweenness-centrality computation. Our experiments show that the best generated variants can be competitive with handwritten code for these problems from other research groups; for some inputs, they even outperform the handwritten versions.
From clarity to efficiency for distributed algorithms
Authors: Liu Yanhong A. , Stoller Scott D. , Lin Bo , Gorbovitski Michael
Published: November 2012

This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly.

We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.