bluuebunny/crossref_metadata_2025 huggingface dataset:
Solvent and electrode influence on electrochemical forming of poly-Fe(III)-aminophenylporphyrin films
Authors: Kuzmin Sergey M. , Chulovskaya Svetlana A. , Tesakova Mariya V. , Semeikin Aleksandr S. , Parfenyuk Vladimir I.
Published: August 2017

Fe(III)-complexes of amino-substituted tetraphenylporphyrins obtained from solutions in organic solvents: dichloromethane, ethanol, and dimethyl sulfoxide have been electropolymerized. The solvents’ effects on deposition and surface morphology of the obtained polyporphyrin film have been determined. It is only possible to obtain a polyporphyrin film from DMSO solutions through electrochemical activation of electropolymerization by a superoxide anion radical (O[Formula: see text]. The activation effect of the dissolved oxygen becomes evident in porphyrin interaction with the superoxide anion radical (O[Formula: see text] that is synthesized in DMSO thanks to the quasi-reversible redox process. The size of particles forming the film is lowest when the film is deposited from DMSO and highest when it is deposited from dichloromethane. Therefore, the ratio of polyporphyrin phase grain growth rate to the nucleation rate has the highest value when the film is deposited from dichloromethane. Such films have the most developed surfaces, while those deposited from ethanol are the smoothest. If the film is deposited on an ITO-electrode, the particles forming the surface are a little larger than in the case of deposition on Pt, which is explained by a slower nucleation on the ITO surface. FeClT([Formula: see text]-NH2Ph)P-based films obtained from ethanol and dichloromethane have negative photo-EMF values, which indicates that the [Formula: see text]-type films have semiconductor properties.
Near-Optimal Co-Deployment of Chargers and Sink Stations in Rechargeable Sensor Networks
Authors: Li Songyuan , Fu Lingkun , He Shibo , Sun Youxian
Published: August 2017

Wireless charging technology has drawn great attention of both academia and industry in recent years, due to its potential of significantly improving the system performance of sensor networks. The emergence of an open-source experimental platform for wireless rechargeable sensor networks, Powercast, has made the theoretical research closer to reality. This pioneering platform is able to recharge sensor nodes much more efficiently and allows different communication protocols to be implemented upon users’ demands. Different from the RFID-based model widely used in the existing works, Powercast designs the charger and sink station separately. This leads to a new design challenge of cooperatively deploying minimum number of chargers and sink stations in wireless rechargeable sensor networks. Such a co-deployment issue is extremely challenging, since the deployments of chargers and sink stations are coupled, and each subproblem is known to be NP-hard. The key to the design is to understand the intrinsic relationship between data flow and energy flow, which is interdependent. In this article, we tackle this challenge by dividing it into two subproblems and optimizing charger and sink station deployment iteratively. Specifically, we first transform each subproblem to a max-flow problem. With this, we are able to select chargers or sink stations according to their contributions to the total flow rate. We design greedy-based algorithms with a guaranteed worst-case bound
ln R/ξ
for the subproblems of charger deployment and sink station deployment, respectively. Further, we address the original problem by designing an iterative algorithm that solves two subproblems alternatively to achieve a near optimal performance. We corroborate our analysis by extensive simulations under practical coefficient settings and demonstrate the advantage of the proposed algorithm.
Scaling up functional programming education: under the hood of the OCaml MOOC
Authors: Canou Benjamin , Di Cosmo Roberto , Henry Grégoire
Published: August 2017

This article describes the key innovations used in the massive open online course ``Introduction to Functional Programming using OCaml'' that has run since the fall semester of 2015. A fully in-browser development environment with an integrated grader provides an exceptional level of feedback to the learners. A functional library of grading combinators greatly simplifies the notoriously complex task of writing test suites for the exercises, and provides static type-safety guarantees on the tested user code. Even the error-prone manual process of importing the course content in the learning platform has been replaced by a functional program that describes the course and statically checks its contents. A detailed statistical analysis of the data collected during and after the course assesses the effectiveness of these innovations.
A framework for adaptive differential privacy
Authors: Winograd-Cort Daniel , Haeberlen Andreas , Roth Aaron , Pierce Benjamin C.
Published: August 2017

Differential privacy is a widely studied theory for analyzing sensitive data with a strong privacy guarantee—any change in an individual's data can have only a small statistical effect on the result—and a growing number of programming languages now support differentially private data analysis. A common shortcoming of these languages is poor support for
adaptivity
. In practice, a data analyst rarely wants to run just one function over a sensitive database, nor even a predetermined sequence of functions with fixed privacy parameters; rather, she wants to engage in an interaction where, at each step, both the choice of the next function and its privacy parameters are informed by the results of prior functions. Existing languages support this scenario using a
simple composition theorem
, which often gives rather loose bounds on the actual privacy cost of composite functions, substantially reducing how much computation can be performed within a given privacy budget. The theory of differential privacy includes other theorems with much better bounds, but these have not yet been incorporated into programming languages.

We propose a novel framework for adaptive composition that is elegant, practical, and implementable. It consists of a reformulation based on typed functional programming of
privacy filters
, together with a concrete realization of this framework in the design and implementation of a new language, called
Adaptive Fuzz
. Adaptive Fuzz transplants the core static type system of Fuzz to the adaptive setting by wrapping the Fuzz typechecker and runtime system in an outer
adaptive layer
, allowing Fuzz programs to be conveniently constructed and typechecked on the fly. We describe an interpreter for Adaptive Fuzz and report results from two case studies demonstrating its effectiveness for implementing common statistical algorithms over real data sets.
Symbolic conditioning of arrays in probabilistic programs
Authors: Narayanan Praveen , Shan Chung-chieh
Published: August 2017

Probabilistic programming systems make machine learning more modular by automatinginference. Recent work by Shan and Ramsey makes inference more modular by automatingconditioning. Their technique uses a symbolic program transformation that treats conditioning generally via the measure-theoretic notion ofdisintegration. This technique, however, is limited to conditioning a single scalar variable. As a step towards modular inference for realistic machine learning applications, we have extended the disintegration algorithm to symbolically condition arrays in probabilistic programs. The extended algorithm implementslifted disintegration, where repetition is treated symbolically and without unrolling loops. The technique uses a language ofindex variablesfor tracking expressions at various array levels. We find that the method works well for arbitrarily-sized arrays of independent random choices, with the conditioning step taking time linear in the number of indices needed to select an element.
Verified low-level programming embedded in F*
Authors: Protzenko Jonathan , Zinzindohoué Jean-Karim , Rastogi Aseem , Ramananandro Tahina , Wang Peng , Zanella-Béguelin Santiago , Delignat-Lavaud Antoine , Hriţcu Cătălin , Bhargavan Karthikeyan , Fournet Cédric , Swamy Nikhil
Published: August 2017

We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently- typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code.

By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.

We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.
Better living through operational semantics: an optimizing compiler for radio protocols
Authors: Mainland Geoffrey
Published: August 2017

Software-defined radio (SDR) promises to bring the flexibility and rapid iterative workflow of software to radio protocol design. Many factors make achieving this promise challenging, not least of which are the high data rates and timing requirements of real-world radio protocols. The Ziria language and accompanying compiler demonstrated that a high-level language can compete in this demanding space, but extracting reusable lessons from this success is difficult due to Ziria's lack of a formal semantics. Our first contribution is a core language, operational semantics, and type system for Ziria.

The insight we gained through developing this operational semantics led to our second contribution, consisting of two program transformations. The first is fusion, which can eliminate intermediate queues in Ziria programs. Fusion subsumes many one-off optimizations performed by the original Ziria compiler. The second transformation is pipeline coalescing, which reduces execution overhead by batching IO. Pipeline coalescing relies critically on fusion and provides a much simpler story for the original Ziria compiler's "vectorization" transformation. These developments serve as the basis of our third contribution, a new compiler for Ziria that produces significantly faster code than the original compiler. The new compiler leverages our intermediate language to help eliminate unnecessary memory traffic.

As well as providing a firm foundation for the Ziria language, our work on an operational semantics resulted in very real software engineering benefits. These benefits need not be limited to SDR---the core language and accompanying transformations we present are applicable to other domains that require processing streaming data at high speed.
A relational logic for higher-order programs
Authors: Aguirre Alejandro , Barthe Gilles , Gaboardi Marco , Garg Deepak , Strub Pierre-Yves
Published: August 2017

Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.

We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation
Authors: Hamana Makoto
Published: August 2017

We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories.

To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of second-order computation in a non-trivial manner. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and lambda-calculi, Plotkin and Power's theory of states, and Stark's theory of pi-calculus.
SpaceSearch: a library for building and verifying solver-aided tools
Authors: Weitz Konstantin , Lyubomirsky Steven , Heule Stefan , Torlak Emina , Ernst Michael D. , Tatlock Zachary
Published: August 2017

Many verification tools build on automated solvers. These tools reduce problems in a specific application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the reductions themselves is rarely verified in practice, limiting the confidence that the solver's output establishes the desired domain-level property.

This paper presents SpaceSearch, a new library for developing solver-aided tools within a proof assistant. A user builds their solver-aided tool in Coq against the SpaceSearch interface, and the user then verifies that the results provided by the interface are sufficient to establish the tool's desired high-level properties. Once verified, the tool can be extracted to an implementation in a solver-aided language (e.g., Rosette), where SpaceSearch provides an efficient instantiation of the SpaceSearch interface with calls to an underlying SMT solver. This combines the strong correctness guarantees of developing a tool in a proof assistant with the high performance of modern SMT solvers. This paper also introduces new optimizations for such verified solver-aided tools, including parallelization and incrementalization.

We evaluate SpaceSearch by building and verifying two solver-aided tools. The first, SaltShaker, checks that RockSalt's x86 semantics for a given instruction agrees with STOKE's x86 semantics. SaltShaker identified 7 bugs in RockSalt and 1 bug in STOKE. After these systems were patched by their developers, SaltShaker verified the semantics' agreement on 15,255 instruction instantiations in under 2h. The second tool, BGProof, is a verified version of an existing Border Gateway Protocol (BGP) router configuration checker. Like the existing checker, BGProof scales to checking industrial configurations spanning over 240 KLOC, identifying 19 configuration inconsistencies with no false positives. However, the correctness of BGProof has been formally proven, and we found 2 bugs in the unverified implementation. These results demonstrate that SpaceSearch is a practical approach to developing efficient, verified solver-aided tools.
Super 8 languages for making movies (functional pearl)
Authors: Andersen Leif , Chang Stephen , Felleisen Matthias
Published: August 2017

The Racket doctrine tells developers to narrow the gap between the terminology of a problem domain and general programming constructs by creating languages instead of just plain programs. This pearl illustrates this point with the creation of a relatively simple domain-specific language for editing videos. To produce the video proceedings of a conference, for example, video professionals traditionally use "non-linear" GUI editors to manually edit each talk, despite the repetitive nature of the process. As it turns out, video editing naturally splits the work into a declarative phase and an imperative rendering phase at the end. Hence it is natural to create a functional-declarative language for the first phase, which reduces a lot of manual labor. This user-facing DSL utilizes a second, internal DSL to implement the second phase, which is an interface to a general, low-level C library. Finally, we inject type checking into our language via another DSL that supports programming in the language of type formalisms. In short, the development of the video editing language cleanly demonstrates how the Racket doctrine naturally leads to the creation of language hierarchies, analogous to the hierarchies of modules found in conventional functional languages.
An Efficient Computation Framework for Connection Discovery using Shared Images
Authors: Cheung Ming , Li Xiaopeng , She James
Published: August 2017

With the advent and popularity of the social network, social graphs become essential to improve services and information relevance to users for many social media applications to predict follower/followee relationship, community membership, and so on. However, the social graphs could be hidden by users due to privacy concerns or kept by social media. Recently, connections discovered from user-shared images using machine-generated labels are proved to be more accessible alternatives to social graphs. But real-time discovery is difficult due to high complexity, and many applications are not possible. This article proposes an efficient computation framework for connection discovery using user-shared images, which is suitable for any image processing and computer vision techniques for connection discovery on the fly. The framework includes the architecture of online computation to facilitate real-time processing, offline computation for a complete processing, and online/offline communication. The proposed framework is implemented to demonstrate its effectiveness by speeding up connection discovery through user-shared images. By studying 300K+ user-shared images from two popular social networks, it is proven that the proposed computation framework reduces 90% of runtime with a comparable accurate with existing frameworks.
Short-term changes in diet composition do not affect in vivo hepatic protein synthesis in rats
Authors: Estrada Andrea Lee , Hudson William Max , Kim Paul Y. , Stewart Claire Marie , Peelor Frederick F. , Wei Yuren , Wang Dong , Hamilton Karyn L. , Miller Benjamin F. , Pagliassotti Michael J.
Published: August 2017

Protein synthesis is critical to protein homeostasis (proteostasis), and modifications in protein synthesis influence lifespan and the development of comorbidities associated with obesity. In the present study, we examined the acute response of liver protein synthesis to either high-fat or high-sucrose diets in order to elucidate nutrient-mediated regulation of hepatic protein synthesis in the absence of body fat accumulation. Total and endoplasmic reticulum-associated protein syntheses were assessed by use of the stable isotope, deuterium oxide (2H2O), in rats provided a control diet or diets enriched in polyunsaturated fat, saturated fat, or sucrose for 2, 4, or 7 days. The three experimental diets increased hepatic triglycerides 46–91% on day 7 and fasting insulin levels 83–117% on day 7, but did not result in differences in body weight when compared with control ( n = 6/diet/time). The fraction of newly synthesized proteins in total liver lysates and microsomes was not significantly different among dietary groups ( n = 3/diet/time). To determine whether the experimental diets provoked a transcriptional response to enhance the capacity for protein synthesis, we also measured a panel of genes linked to amino acid transport, synthesis, and processing. There were no significant differences in any of the genes measured among groups. Therefore, dietary treatments that have been linked to impaired proteostasis and that promote hepatic steatosis and insulin resistance, did not result in significant changes in total or ER-associated protein synthesis in the liver over a 7-day period.
Positive Effect of Higher Adult Body Mass Index on Overall Survival of Digestive System Cancers Except Pancreatic Cancer: A Systematic Review and Meta-Analysis
Authors: Han Jie , Zhou Yumei , Zheng Yuxiu , Wang Miaomiao , Cui Jianfeng , Chen Pengxiang , Yu Jinming
Published: August 2017

High body mass index (BMI) has been inconsistently associated with overall survival (OS) of digestive system cancers (DSCs). This meta-analysis was conducted to investigate whether high BMI was associated with DSCs prognosis. 34 studies were accepted, with a total of 23,946 DSC cases. Hazard ratios (HRs) with 95% confidence intervals (95% CIs) for OS in BMI categories from individual studies were extracted and pooled by random-effect model. The overall HR of DSCs except pancreatic cancer for OS of adult overweight cases was 0.76 (95% CI = 0.67–0.85). DSC individuals except pancreatic cancer with adult obesity were at decreased risk for OS (HR = 0.85, 95% CI = 0.72–0.98). Among DSC patients except pancreatic cancer, the overall HR for the highest versus the lowest BMI category was 0.82 (95% CI = 0.71–0.92). Additionally, comparing the highest and lowest BMI categories, the combined HR of pancreatic cancer was 1.22 (95% CI = 1.01–1.43). Our meta-analysis suggested an increased OS among adult overweight and obese DSC survivors except pancreatic cancer. Overweight and obesity in adulthood may be important prognostic factors that indicate an increased survival from DSC patients except pancreatic cancer.
Lycopene Inhibits Propagation of Chlamydia Infection
Authors: Zigangirova Naylia A. , Morgunova Elena Y. , Fedina Elena D. , Shevyagina Natalia V. , Borovaya Tatiana G. , Zhukhovitsky Vladimir G. , Kyle Nigel H. , Petyaev Ivan M.
Published: August 2017

Chlamydiaceae is a family of obligate intracellular pathogenic bacteria with similar developmental cycles and cell biology responsible for a wide range of diseases in different hosts including genital and eye inflammatory diseases, arthritis, and inflammatory diseases of the respiratory and cardiovascular systems. In the present paper, we report that lycopene, one of the main dietary carotenoids, which is present in tomato and some other fruits, has a strong inhibitory effect onC. trachomatisandC. pneumoniaeinfections in alveolar macrophages. This finding was documented by both immunofluorescence analysis and electron microscopy. It was noted that lycopene treatment inhibited intracellular phase of the chlamydial developmental cycle and resulted in a significant loss of infectious progeny. The antichlamydial effect of lycopene was also confirmed in a clinical setting. There was a significant reduction of IgG antibodies againstC. pneumoniaein the serum of volunteers treated for a month with oral ingestion of 7 mg of lycopene. Additional studies are needed to further explore the antichlamydial activity of lycopene and its possible effect onC. pneumoniaein relation to antichlamydial activity of lycopene to mechanisms of atherosclerosis.
Readability and Suitability of COPD Consumer Information
Authors: Fullmann Kathryn , Blackburn David F. , Fenton Mark E. , Mansell Holly
Published: August 2017

Background. Information leaflets have been shown to positively or negatively impact adherence, depending on their content. The objective of this study was to perform an appraisal of the consumer information provided in COPD inhaler monographs. Methods. COPD inhalers were identified from the Health Canada Drug Product Database. Medication information and instructions for inhaler use were analyzed for readability by seven formulas, with an acceptability threshold of grades 6–8. Three researchers rated suitability using a modified Suitability Assessment of Materials (SAM) tool and assessed leaflets for explicit warnings. Results. Twenty-six inhalers with a COPD indication were evaluated. Medication information sections were rated as “difficult to read” or “hard,” and 85% (22/26) had a reading level above grade 8. The instructions for inhaler use were rated as “easy” or “fairly easy” to read and 63% (16/26) met the threshold by all formulas. While all leaflets achieved superior suitability ratings, extreme warnings included risk of premature death (n=12), risks of serious injury (n=26), serious interactions (n=26), and statements that convey a serious consequence to therapy (n=26). Conclusion. While COPD information leaflets in Canada performed well in terms of readability and suitability, overemphasis on side effects, warnings, and precautions may contribute to patient fear and nonadherence.
The Relationship between Polar Vortex and Ozone Depletion in the Antarctic Stratosphere during the Period 1979–2016
Authors: Zhang Yu , Li Jing , Zhou Libo
Published: August 2017

As the most prominent feature of the polar stratosphere, polar vortex results in widespread changes in the climate system, especially in the ozone variation. In this study, the linkage between polar vortex and ozone depletion in Antarctic stratosphere during the period 1979–2016 is investigated; we calculated the averaged total column ozone within the polar vortex based on the vortex edge (−28.8 PVU PV contour) instead of the geographical region defined by latitude and longitude. Results from the spatial patterns of ozone and polar vortex suggest that the morphological changes of polar vortex can impact the horizontal distribution of ozone and the ozone within the polar vortex experiences a severe depletion in spring. The negative relationship between ozone and polar vortex in terms of vortex area, strength, and breakup time is significant with the correlation coefficients of −0.57, −0.68, and −0.76, respectively. The breakup time of polar vortex plays an important role in the relation between polar vortex and ozone depletion with the highest-value correlation coefficient among three polar vortex parameters. Furthermore, the possible mechanism for this relationship is also discussed in this article.
All-Pass Filter Based Linear Voltage Controlled Quadrature Oscillator
Authors: Mathur Koushick , Venkateswaran Palaniandavar , Nandi Rabindranath
Published: August 2017

A linear voltage controlled quadrature oscillator implemented from a first-order electronically tunable all-pass filter (ETAF) is presented. The active element is commercially available current feedback amplifier (AD844) in conjunction with the relatively new Multiplication Mode Current Conveyor (MMCC) device. Electronic tunability is obtained by the control node voltage (V) of the MMCC. Effects of the device nonidealities, namely, the parasitic capacitors and the roll-off poles of the port-transfer ratios of the device, are shown to be negligible, even though the usable high-frequency ranges are constrained by these imperfections. Subsequently the filter is looped with an electronically tunable integrator (ETI) to implement the quadrature oscillator (QO). Experimental responses on the voltage tunable phase of the filter and the linear-tuning law of the quadrature oscillator up to 9.9 MHz at low THD are verified by simulation and hardware tests.
Macrodamage Accumulation Model for a Human Femur
Authors: Hamandi Farah , Goswami Tarun
Published: August 2017

The objective of this study was to more fully understand the mechanical behavior of bone tissue that is important to find an alternative material to be used as an implant and to develop an accurate model to predict the fracture of the bone. Predicting and preventing bone failure is an important area in orthopaedics. In this paper, the macrodamage accumulation models in the bone tissue have been investigated. Phenomenological models for bone damage have been discussed in detail. In addition, 3D finite element model of the femur prepared from imaging data with both cortical and trabecular structures is delineated using MIMICS and ANSYS® and simulated as a composite structure. The damage accumulation occurring during cyclic loading was analyzed for fatigue scenario. We found that the damage accumulates sooner in the multiaxial than in the uniaxial loading condition for the same number of cycles, and the failure starts in the cortical bone. The damage accumulation behavior seems to follow a three-stage growth: a primary phase, a secondary phase of damage growth marked by linear damage growth, and a tertiary phase that leads to failure. Finally, the stiffness of the composite bone comprising the cortical and trabecular bone was significantly different as expected.
Reverse Total Shoulder Arthroplasty as Treatment for Rotator Cuff-Tear Arthropathy and Shoulder Dislocations in an Elderly Male with Parkinson’s Disease
Authors: Skedros John G. , Smith James S. , Langston Tanner D. , Adondakis Micheal G.
Published: August 2017

We report the case of a 70-year-old male with Parkinson’s disease (PD) and recurrent traumatic left shoulder dislocations. This case is rare because (1) he had a massive irreparable rotator cuff tear and end-stage arthritis (i.e., rotator cuff-tear arthropathy) of the same shoulder and (2) his shoulder was ultimately reconstructed with a reverse total shoulder arthroplasty (RTSA). His first dislocation occurred after a fall. Recurrent shoulder dislocations occurred despite successful closed reduction and physical therapy. Initial surgical treatment included an open capsular-labral reconstruction; RTSA was not an ideal option because of the presumed risk of failure from PD-related dyskinesias. However, the capsular-labral reconstruction failed after he lost balance and stumbled but did not fall. A RTSA was then done which restored the patient’s shoulder stability and greatly improved his pain. At final follow-up two years later, he reported pain relief and improved function. This was partially attributed to the fact that he had moved to an assisted living center. He also began using an electric wheelchair one year after the RTSA. We report this case because of the unusual set of conditions and circumstances, namely, the implantation of a RTSA in a patient with PD and shoulder instability.
Research on the Adaptive Damping Method of Strap-Down Inertial Measurement Unit Based on the Magneto Rheological Technology
Authors: Zhang Heng , Rui Xiaoting , Yang Fufeng , Chen Gangli
Published: August 2017

To improve the output accuracy of strap-down inertial measurement unit which is in compound dynamic environment of missile which has a high acceleration, strong impact, and high vibration, an adaptive damping method of taking the magneto rheological elastomer as the vibration damper is designed. This method takes the error between the vibration response of the missile and the dynamic response of SIMU as the performance index of optimal control. By optimal control, the stiffness and damping of the magneto rheological elastomer are automatically adjusted, the vibration response of the SIMU is controlled, and the output accuracy of SIMU is improved. Results of experiments show that the method solves the problem that the stiffness and damping of the SIMU damping system could not be changed in real time to adapt to the dynamic environment, and there is almost no time delay and this has an obvious damping effect.
Gastric Metastasis from Renal Cell Carcinoma, Clear Cell Type, Presenting with Gastrointestinal Bleeding
Authors: Abu Ghanimeh Mouhanna , Qasrawi Ayman , Abughanimeh Omar , Albadarin Sakher , Helzberg John H.
Published: August 2017

Renal cell carcinoma (RCC) accounts for 80–85% of all primary renal neoplasms. Although RCC can metastasize to any organ, gastric metastases from RCC are exceedingly rare. A 67-year-old male presented with melena and acute blood loss anemia. The patient had a history of RCC that had been treated with a radical nephrectomy. He had a recent myocardial infarction and was receiving double antiplatelet therapy. After hemodynamic stabilization, esophagogastroduodenoscopy showed a polypoid mass in the gastric fundus. The mass was excised. Histological and immunohistochemical evaluation were consistent with clear cell RCC. The polypoid lesion is consistent with a late solitary metastasis.
The Association of Thyrotropin and Autoimmune Thyroid Disease in Developing Papillary Thyroid Cancer
Authors: Lee I-Shuan , Hsieh An-Tsz , Lee Ting-Wei , Lee Ting-I , Chien Yu-Mei
Published: August 2017

Background. Papillary thyroid carcinoma (PTC) is the most common type of malignant thyroid neoplasm. However, the incidence of PTC with autoimmune thyroid disease (AITD) varies between studies. This study aims to investigate whether patients with AITD have increased incidence of PTC. We also analyzed the relationship of serum thyroid-stimulating hormone (TSH) levels and PTC in relation to AITD based on histopathological data. Methods. A total of 533 participants who underwent thyroidectomy were enrolled in this retrospective study based on clinicohistopathological data and known thyroid autoantibodies. Patients were divided into PTC and benign groups according to histopathologic diagnosis. Age, gender, body mass index, and serum TSH level before thyroidectomy were recorded. Results. Of the 533 enrolled patients, 159 (29.8%) were diagnosed with PTC, of which 38 (35.5%) had Hashimoto’s thyroiditis (HT). More patients with HT were female, and patients with HT, Graves’ disease, and thyroid nodules with higher TSH level had a higher incidence of PTC. Conclusions. A high proportion of the patients with PTC had HT. There was a trend that a higher serum TSH level was associated with a greater risk of thyroid cancer.
Improvements for Finding Impossible Differentials of Block Cipher Structures
Authors: Luo Yiyuan , Lai Xuejia
Published: August 2017

We improve Wu and Wang’s method for finding impossible differentials of block cipher structures. This improvement is more general than Wu and Wang’s method where it can find more impossible differentials with less time. We apply it on Gen-CAST256, Misty, Gen-Skipjack, Four-Cell, Gen-MARS, SMS4, MIBS, Camellia⁎, LBlock, E2, and SNAKE block ciphers. All impossible differentials discovered by the algorithm are the same as Wu’s method. Besides, for the 8-round MIBS block cipher, we find 4 new impossible differentials, which are not listed in Wu and Wang’s results. The experiment results show that the improved algorithm can not only find more impossible differentials, but also largely reduce the search time.
Designing Dynamic Delivery Parking Spots in Urban Areas to Reduce Traffic Disruptions
Authors: Roca-Riu Mireia , Cao Jin , Dakic Igor , Menendez Monica
Published: August 2017

Pick-up and delivery services are essential for businesses in urban areas. However, due to the limited space in city centers, it might be unfeasible to provide sufficient loading/unloading spots. As a result, this type of operations often interferes with traffic by occupying road space (e.g., illegal parking). In this study, a potential solution is investigated: Dynamic Delivery Parking Spots (DDPS). With this concept, based on the time-varying traffic demand, the area allowed for delivery parking changes over time in order to maximize delivery opportunities while reducing traffic disruptions. Using the hydrodynamic theory of traffic flow, we analyze the traffic discharging rate on an urban link with DDPS. In comparison to the situation without delivery parking, the results show that although DDPS occupy some space on a driving lane, it is possible to keep the delay at a local level, that is, without spreading to the network. In this paper, we provide a methodology for the DDPS design, so that the delivery requests can be satisfied while their negative impacts on traffic are reduced. A simulation study is used to validate the model and to estimate delay compared to real situations with illegal parking, showing that DDPS can reduce system’s delay.
Neutrophil-to-Lymphocyte Ratio Predicts Prognosis in Castration-Resistant Prostate Cancer Patients Who Received Cabazitaxel Chemotherapy
Authors: Uemura Koichi , Kawahara Takashi , Yamashita Daisuke , Jikuya Ryosuke , Abe Koichi , Tatenuma Tomoyuki , Yokomizo Yumiko , Izumi Koji , Teranishi Jun-ichi , Makiyama Kazuhide , Yumura Yasushi , Kishida Takeshi , Udagawa Koichi , Kobayashi Kazuki , Miyoshi Yasuhide , Yao Masahiro , Uemura Hiroji
Published: August 2017

Introduction and Objectives. An elevated neutrophil-to-lymphocyte ratio (NLR) has been suggested to be associated with a poor prognosis in several cancers. We evaluated the utility of an elevated NLR as a biomarker to predict the prognosis of metastatic castration-resistant prostate cancer (mCRPC) patients treated with cabazitaxel (CBZ). Methods. We analyzed 47 patients who received CBZ chemotherapy for mCRPC in our institutions. The NLR was calculated using the neutrophil and lymphocyte counts before CBZ chemotherapy. We determined the NLR cut-off value based on the sensitivity and specificity levels derived from area under the receiver operator characteristic curves for death. A multivariate analysis was performed to investigate the association between the NLR and the prognosis. Results. The median overall survival (OS) after CBZ was 10.0 months (range: 6.3–13.2). The median OS was shorter in patients with a high NLR (≥3.83) than in those with a low NLR (<3.83) (5.8 versus 13.2 months, p=0.018). In the multivariate analysis, the NLR, patient age, and lymph node (LN) metastasis were independent predictors of the OS (hazard ratio 3.01, p=0.030; hazard ratio 3.10, p=0.029; hazard ratio 12.38, p=0.001, resp.). Conclusions. NLR might be a useful prognostic biomarker in mCRPC patients treated with CBZ.
IGF1 and NRG1 Enhance Proliferation, Metabolic Maturity, and the Force-Frequency Response in hESC-Derived Engineered Cardiac Tissues
Authors: Rupert Cassady E. , Coulombe Kareen L. K.
Published: August 2017

Insulin-like growth factor 1 (IGF1) and neuregulin-1β (NRG1) play important roles during cardiac development both individually and synergistically. In this study, we analyze how 3D cardiac tissue engineered from human embryonic stem cell- (hESC-) derived cardiomyocytes and 2D-plated hESC-cardiomyocytes respond to developmentally relevant growth factors both to stimulate maturity and to characterize the therapeutic potential of IGF1 and NRG1. When administered to engineered cardiac tissues, a significant decrease in active force production of ~65% was measured in all treatment groups, likely due to changes in cellular physiology. Developmentally related processes were identified in engineered tissues as IGF1 increased hESC-cardiomyocyte proliferation 3-fold over untreated controls and NRG1 stimulated oxidative phosphorylation and promoted a positive force-frequency relationship in tissues up to 3 Hz. hESC-cardiomyocyte area increased significantly with NRG1 and IGF1 + NRG1 treatment in 2D culture and gene expression data suggested increased cardiac contractile components in engineered tissues, indicating the need for functional analysis in a 3D platform to accurately characterize engineered cardiac tissue response to biochemical stimulation. This study demonstrates the therapeutic potential of IGF1 for boosting proliferation and NRG1 for promoting metabolic and contractile maturation in engineered human cardiac tissue.
Prospective 3D Investigation of Bleb Wall after Trabeculectomy Using Anterior-Segment OCT
Authors: Watanabe-Kitamura Fumika , Inoue Toshihiro , Kojima Sachi , Nakashima Kei-Ichi , Fukushima Ayako , Tanihara Hidenobu
Published: August 2017

Purpose. We used three-dimensional anterior-segment optical coherence tomography (3D AS-OCT) to evaluate time-dependent posttrabeculectomy changes in bleb wall volume and intensity. Methods. This prospective observational study included patients with open-angle glaucoma who underwent fornix-based trabeculectomy between January 2012 and October 2012. Twenty-nine eyes met inclusion criteria, and the bleb walls of 22 were amenable to three-dimensional analysis by 3D AS-OCT for 1 year after surgery. The high-intensity volume ratio was calculated as the proportion of the high-intensity region in the total bleb wall. Changes in the high-intensity volume ratio were of high intensity, and parameters influencing the ratio were analyzed using 3D AS-OCT. Results. The mean high-intensity volume ratios (±SDs) were 43.5 ± 21.4, 44.1 ± 14.8, 41.5 ± 22.6, and 43.2 ± 19.7% at 0.5, 3, 6, and 12 months after trabeculectomy, respectively. When the volume ratios obtained 0.5 and 12 months posttrabeculectomy were compared, four and five eyes exhibited decreases and increases of over 20%, respectively. The volume ratios at 12 months correlated with the intraocular pressure (IOP) at that time (t=2.44, P=0.024) and the bleb wall vascularity score at 12 months (t=5.44, P<0.001). Conclusions. The high-intensity bleb wall at 12 months posttrabeculectomy reflected the IOP and the bleb wall vascularity at that time.
Vegetation Dynamics and Their Response to Climatic Variability in China
Authors: Zhang Bowen , Cui Linli , Shi Jun , Wei Peipei
Published: August 2017

Based on SPOT VEGETATION data and meteorological data, NDVI (Normalized Difference Vegetation Index) and its response to temperature and precipitation in China and its different regions were investigated over the period 1998–2013 by using the maximum value composite and linear regression methods. The results showed that NDVI presented significant increase (0.0046/a) for all of China and all the regions over the last 16 years. Meanwhile, annual mean temperature of China presented a slightly increasing trend, while the annual precipitation showed a slightly decreasing trend over the last 16 years. Nevertheless, there were differences between temperature and precipitation in the subregions of China. The Annual NDVI had better relationships with precipitation (r=0.126) compared to temperature (r=-0.094), and NDVI also had a good correlation with precipitation rather than temperature in different subregions of China. Additionally, human activities also made a difference to the trends of NDVI in some regions. This study is conductive to the effects of climate change on vegetation activity in future research.
Intrastromal Corneal Ring Segments for Astigmatism Correction after Deep Anterior Lamellar Keratoplasty
Authors: Arantes Júlio C. D. , Coscarelli Sandro , Ferrara Paulo , Araújo Luana P. N. , Ávila Marcos , Torquetti Leonardo
Published: August 2017

Background. To evaluate the change in corneal astigmatism after intrastromal corneal ring segment (ICRS) implantation in keratoconus patients with previous deep anterior lamellar keratoplasty (DALK). Design was a longitudinal, retrospective, interventional study. The study included 25 eyes of 24 patients with keratoconus who had DALK performed at least two years prior to ICRS implantation. All patients had a clear corneal graft with up to 8.00 D of corneal astigmatism and intolerance to contact lenses. The studied parameters were age, sex, corrected distance visual acuity (CDVA), maximum keratometry (K1), minimum keratometry (K2), spherical equivalent, and astigmatism. There was a statistically significant decrease in the postintervention analysis as follows: 3.5 D reduction in K1 (p<0.001); 1.53 D in K2 (p=0.005); and 2.52 D (p<0.001) in the average K. The spherical equivalent reduced from −3.67 D (±2.74) to −0.71 D (±2.35) (p<0.001). The topographic astigmatism reduced from 3.87 D preoperatively to 1.90 D postoperatively (p<0.001). The CDVA improved from 0.33 (±0.10) to 0.20 (±0.09, p<0.001). ICRS implantation is a useful option for the correction of astigmatism after DALK as it yields significant visual, topographic, and refractive results.
Reverse Segond Fracture Associated with Anteromedial Tibial Rim and Tibial Attachment of Anterior Cruciate Ligament Avulsion Fractures
Authors: Bedeir Yehia H.
Published: August 2017

Reverse Segond fracture is an uncommon avulsion fracture of the tibial attachment of the deep portion of the medial collateral ligament of the knee. We report a reverse Segond fracture associated with anterior cruciate ligament tibial avulsion fracture and anteromedial tibial rim fracture. Unlike previous reports, the combination of reverse Segond fracture, anteromedial tibial rim fracture, and anterior cruciate ligament avulsion fracture was not associated with posterior cruciate ligament injury, posterolateral corner injury, or tibial plateau fracture. This new combination of injuries provides better understanding of the mechanisms of ligamentous injuries of the knee and highlights the importance of meticulous assessment of these injuries for accurate diagnosis and subsequent management.
The Least Squares Hermitian (Anti)reflexive Solution with the Least Norm to Matrix Equation AXB = C
Authors: Liu Xin , Wang Qing-Wen
Published: August 2017

For a given generalized reflection matrix J, that is, JH = J, J2 = I, where JH is the conjugate transpose matrix of J, a matrix A ∈ Cn×n is called a Hermitian (anti)reflexive matrix with respect to J if AH = A and A = ±JAJ. By using the Kronecker product, we derive the explicit expression of least squares Hermitian (anti)reflexive solution with the least norm to matrix equation AXB = C over complex field.