bluuebunny/crossref_metadata_2025 huggingface dataset:
Should One Be A Left or A Right Sellarsian? (And is There Really Such A Choice?)
Authors: Peregrin Jaroslav
Published: April 2016

The followers of Wilfrid Sellars are often divided into “right” and “left” Sellarsians, according to whether they believe, in Mark Lance's words, that “linguistic roles constitutive of meaning and captured by dot quoted words are ‘normative all the way down.’” The present article anatomizes this division and argues that it is not easy to give it a nontrivial sense. In particular, the article argues that it is not really possible to construe it as a controversy related to ontology, and goes on to argue that it is also not easy to construe it as one concerning the translatability of the normative idiom into the non‐normative one. The conclusion is that the only coherent interpretation of this disagreement is as a disagreement about the possibility and desirability of assuming a standpoint “inside” our linguistic practices.
Systematic wood anatomy of the subfamily Acalyphoideae s.l. (Euphorbiaceae) from India, with remarks on synonymy
Authors: Jangid Prem Prakash , Gupta Sangeeta
Published: April 2016

The present paper deals with the wood microstructure of 18 species belonging to 8 genera classified in four tribes of the subfamily Acalyphoideae s.l. (Euphorbiaceae). The study mainly focuses on the systematic implications of wood anatomy to the subfamily, but also ecological and evolutionary aspects are evaluated. The wood microstructure of the subfamily was found to be considerably homogeneous except for that of the tribe Chaetocarpeae. The results support the segregation of Hancea from Mallotus and merging of Trewia into Mallotus. It is further suggested to include Mallotus nudiflorus in Mallotus sect. Philippinensis instead of Mallotus sect. Rottleropsis. Wood anatomical data turned out to solve the synonymic problem of Mallotus albus, Mallotus macrostachyus and Mallotus tetracoccus as well as Macaranga denticulata and Macaranga pustulata as the results indicate that these species are all distinct. The sectional circumscriptions of Macaranga and Mallotus are evaluated based on wood anatomical data. Radial laticifers are reported for the first time in Macaranga indica. A species identification key to Indian species of Acalyphoideae based on wood anatomical characteristics is provided.
EZH2 as a mediator of treatment resistance in melanoma
Authors: Tiffen Jessamy C. , Gallagher Stuart J. , Tseng Hsin‐Yi , Filipp Fabian V. , Fazekas de St Groth Barbara , Hersey Peter
Published: April 2016

Direct treatments of cancer such as chemotherapy, radiotherapy and targeted therapy have been shown to depend on recruitment of the immune system for their effectiveness. Recent studies have shown that development of resistance to direct therapies such as BRAF inhibitors in melanoma is associated with suppression of immune responses. We point to emerging data that implicate activation of the polycomb repressive complex 2 (PRC2) and its catalytic component—enhancer of zeste homolog 2 (EZH2)—in progression of melanoma and suppression of immune responses. EZH2 appears to have an important role in differentiation of CD4 T cells and particularly in the function of T regulatory cells, which suppress immune responses to melanoma. We review mechanisms of EZH2 activation at the genomic level and from activation of the MAP kinase, E2F or NF‐kB2 pathways. These studies are consistent with activation of EZH2 as a common mechanism for induction of immune suppression in patients failing direct therapies and suggest EZH2 inhibitors may have a role in combination with immunotherapy and targeted therapies to prevent development of immunosuppression.
Effect of Dielectric Electrical Conductivity on the Characteristics of Micro Electro-Discharge Machining Plasma and Material Removal
Authors: Mujumdar Soham S. , Curreli Davide , Kapoor Shiv G.
Published: April 2016

In micro electro-discharge machining (micro-EDM), it is believed that electrical conductivity of the dielectric modified by additives plays an important role in discharge initiation and electrical breakdown, thereby affecting the process characteristics including process accuracy, material removal rate (MRR), and surface finish. However, there has been a lack of systematic efforts to evaluate the effect of dielectric conductivity in micro-EDM. This paper investigates the role of electrical conductivity of the dielectric on the breakdown, plasma characteristics, and material removal in micro-EDM via modeling and experimentation. Experiments have been carried out at four levels of electrical conductivity of saline water, i.e., 4 μS/cm, 362 μS/cm, 1106 μS/cm, and 4116 μS/cm, to study electrical breakdown of the dielectric and resulting craters. A global modeling approach is employed to model the micro-EDM plasma in saline water and predict the effect of dielectric conductivity on electron density, plasma temperature, heat flux to anode, plasma resistance, and discharge energy. It is found from both experiments and model-based simulations that increase in the dielectric conductivity facilitates the electrical breakdown of the dielectric by lowering the minimum breakdown potential at a given interelectrode gap. Experimental results also show increase in the volume of material removed per discharge when dielectric conductivity is increased, which is attributed to the increase in anode heat flux predicted by the micro-EDM plasma model. The model also predicts increase in electron density, decrease in plasma resistance, and decrease in discharge energy as the dielectric conductivity increases.
Assessing the validity of subjective reports in the auditory streaming paradigm
Authors: Farkas Dávid , Denham Susan L. , Bendixen Alexandra , Winkler István
Published: April 2016

While subjective reports provide a direct measure of perception, their validity is not self-evident. Here, the authors tested three possible biasing effects on perceptual reports in the auditory streaming paradigm: errors due to imperfect understanding of the instructions, voluntary perceptual biasing, and susceptibility to implicit expectations. (1) Analysis of the responses to catch trials separately promoting each of the possible percepts allowed the authors to exclude participants who likely have not fully understood the instructions. (2) Explicit biasing instructions led to markedly different behavior than the conventional neutral-instruction condition, suggesting that listeners did not voluntarily bias their perception in a systematic way under the neutral instructions. Comparison with a random response condition further supported this conclusion. (3) No significant relationship was found between social desirability, a scale-based measure of susceptibility to implicit social expectations, and any of the perceptual measures extracted from the subjective reports. This suggests that listeners did not significantly bias their perceptual reports due to possible implicit expectations present in the experimental context. In sum, these results suggest that valid perceptual data can be obtained from subjective reports in the auditory streaming paradigm.
Bronchogenic cyst arising from the crus of the left hemidiaphragm
Authors: Chumakova Maryna , Morris-Stiff Gareth , Khachaturov Vadim , Ibrahim Samuel
Published: April 2016

A 34-year-old man presented with chronic worsening left-sided retrosternal chest pain. Following a negative cardiac work up he was found, on cross-sectional imaging, to have a cystic mass measuring 9.6×11.8×9 cm related to his left diaphragmatic crus. The patient underwent an exploratory laparotomy with complete resection of the cystic mass. Histopathological examination of the mass confirmed it as being a bronchogenic cyst. His pain resolved following excision of the mass and at follow-up he was asymptomatic with no evidence of recurrence on imaging.
Right atrial mass in a patient with breast cancer: percutaneous transcatheter biopsy under intracardiac echocardiography guidance
Authors: Azzalini Lorenzo , de Hemptinne Quentin , Asgar Anita , Ibrahim Reda
Published: April 2016

Precise diagnosis of intracardiac masses is fundamental to their treatment. However, the findings of non-invasive imaging techniques are frequently inconclusive. In this setting, percutaneous transcatheter biopsy might represent a valid alternative to surgical biopsy. Intracardiac echocardiography (ICE)-guided biopsy offers high-quality imaging, is a relatively quick and easy interventional procedure to perform and does not require patient intubation or the assistance of an echocardiographer. We describe the case of a 47-year-old woman undergoing chemotherapy for breast cancer, who presented with a right atrial mass. Non-invasive imaging was inconclusive. Since no changes in the aspect or size of the mass were noticed after 2-week treatment with heparin, ICE-guided biopsy was performed, which confirmed the thrombotic nature of the mass. The patient underwent surgical resection of the thrombus and curative treatment of her breast cancer was pursued.
Simplified Symbolic Gain, CMRR and PSRR Analysis of Analog Amplifiers Using Simulated Annealing
Authors: Shokouhifar Mohammad , Jalali Ali
Published: April 2016

Modeling common-mode rejection ratio (CMRR) and power-supply rejection ratio (PSRR) is of utmost importance during the design of analog integrated circuits. Unfortunately, symbolic analysis suffers from the exponential growing of the complexity of expressions with the circuit size, symbolic simplification techniques should be utilized for the analysis of practical circuits. In this paper, we propose a methodology for the automatic simplified symbolic analysis of gain, CMRR and PSRR in analog amplifiers. We introduce a multi-objective simulated annealing for the simplification of derived symbolic expressions. The fitness function is to minimize the number of symbolic terms while satisfying the optimization constraints. In contrast to the classical criteria which simplify different polynomials separately, the main objective of the proposed criterion is to consider the correlation between different polynomials, during the simplification procedure. The method has been successfully coded in MATLAB and simulated over two analog amplifiers. Comparison of the numerical results extracted from the simplified symbolic expressions with HSPICE demonstrates the efficiency of the proposed methodology.
Effective quantum gravity observables and locally covariant QFT
Authors: Rejzner Kasia
Published: April 2016

Perturbative algebraic quantum field theory (pAQFT) is a mathematically rigorous framework that allows to construct models of quantum field theories (QFTs) on a general class of Lorentzian manifolds. Recently, this idea has been applied also to perturbative quantum gravity (QG), treated as an effective theory. The difficulty was to find the right notion of observables that would in an appropriate sense be diffeomorphism invariant. In this paper, I will outline a general framework that allows to quantize theories with local symmetries (this includes infinitesimal diffeomorphism transformations) with the use of the Batalin–Vilkovisky (BV) formalism. This approach has been successfully applied to effective QG in a recent paper by Brunetti, Fredenhagen and myself. In the same paper, we also proved perturbative background independence of the quantized theory, which is going to be discussed in the present work as well.
Adiabatic and coupled channels calculations for near barrier fusion of 16O +238U using realistic nucleon–nucleon interaction
Authors: Ismail M. , Seif W. M. , Botros M. M.
Published: April 2016

We investigate the fusion cross-section and the fusion barrier distribution of [Formula: see text]O[Formula: see text]U at near- and sub-barrier energies. We use an interaction potential generated by the semi-microscopic double folding model-based on density dependent (DD) form of the realistic Michigan-three-Yukawa (M3Y) Reid nucleon–nucleon (NN) interaction. We studied the role of both the static and dynamic deformations of the target nucleus on the fusion process. Rotational and vibrational degrees of freedom of [Formula: see text]U-nucleus are considered. We found that the deformation and the octupole vibrations in [Formula: see text]U enhance its sub-barrier fusion cross-section. The signature of the the octupole vibrational modes of [Formula: see text]U appears clearly in its fusion barrier distribution profile.
Dynamic surface control and active disturbance rejection control-based integrated guidance and control design and simulation for hypersonic reentry missile
Authors: Zhang Cong , Wu Yun-Jie
Published: April 2016

This paper proposes a novel integrated guidance and control (IGC) method combining dynamic surface control (DSC) and active disturbance rejection control (ADRC) for the guidance and control system of hypersonic reentry missile (HRM) with bounded uncertainties. First, the model of HRM is established. Second, the proposed IGC method based on DSC and ADRC is designed. The stability of closed-loop system is proved strictly. It is worth mentioning that the ADRC technique is used to estimate and compensate the disturbance in the proposed IGC system. This makes the closed-loop system a better performance and reduces the chattering caused by lumped disturbances. Finally, a series of simulations and comparisons with a 6-DOF non-linear missile that includes all aerodynamic effects are demonstrated to illustrate the effectiveness and advantage of the proposed IGC method.
Fully-abstract compilation by approximate back-translation
Authors: Devriese Dominique , Patrignani Marco , Piessens Frank
Published: April 2016

A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full-abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ-calculus (λτ) to the untyped λ-calculus (λu), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back-translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general technique for proving compiler full-abstraction and demonstrate it on a compiler from λτ to λu . The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.
'Cause I'm strong enough: Reasoning about consistency choices in distributed systems
Authors: Gotsman Alexey , Yang Hongseok , Ferreira Carla , Najafzadeh Mahsa , Shapiro Marc
Published: April 2016

Large-scale distributed systems often rely on replicated databases that allow a programmer to request different data consistency guarantees for different operations, and thereby control their performance. Using such databases is far from trivial: requesting stronger consistency in too many places may hurt performance, and requesting it in too few places may violate correctness. To help programmers in this task, we propose the first proof rule for establishing that a particular choice of consistency guarantees for various operations on a replicated database is enough to ensure the preservation of a given data integrity invariant. Our rule is modular: it allows reasoning about the behaviour of every operation separately under some assumption on the behaviour of other operations. This leads to simple reasoning, which we have automated in an SMT-based tool. We present a nontrivial proof of soundness of our rule and illustrate its use on several examples.
Maximal specification synthesis
Authors: Albarghouthi Aws , Dillig Isil , Gurfinkel Arie
Published: April 2016

Many problems in program analysis, verification, and synthesis require inferring specifications of unknown procedures. Motivated by a broad range of applications, we formulate the problem of maximal specification inference: Given a postcondition Phi and a program P calling a set of unknown procedures F_1,…,F_n, what are the most permissive specifications of procedures F_i that ensure correctness of P? In other words, we are looking for the smallest number of assumptions we need to make about the behaviours of F_i in order to prove that $P$ satisfies its postcondition. To solve this problem, we present a novel approach that utilizes a counterexample-guided inductive synthesis loop and reduces the maximal specification inference problem to multi-abduction. We formulate the novel notion of multi-abduction as a generalization of classical logical abduction and present an algorithm for solving multi-abduction problems. On the practical side, we evaluate our specification inference technique on a range of benchmarks and demonstrate its ability to synthesize specifications of kernel routines invoked by device drivers.
Pushdown control-flow analysis for free
Authors: Gilray Thomas , Lyde Steven , Adams Michael D. , Might Matthew , Van Horn David
Published: April 2016

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2^n), PDCFA is in O(n^6), and AAC is in O(n^8). In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n^3) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.
Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
Authors: Chatterjee Krishnendu , Fu Hongfei , Novotný Petr , Hasheminezhad Rouzbeh
Published: April 2016

In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); 2. quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism.
String solving with word equations and transducers: towards a logic for analysing mutation XSS
Authors: Lin Anthony W. , Barceló Pablo
Published: April 2016

We study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is especially relevant when analysing security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer from the reverse problem of being able to model sanitisation functions and browser transductions, but not string concatenations. Naively combining word equations and transducers easily leads to an undecidable logic. Our main contribution is to show that the "straight-line fragment" of the logic is decidable (complexity ranges from PSPACE to EXPSPACE). The fragment can express the program logics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when performing bounded model checking or dynamic symbolic executions. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications. Finally, the logic remains decidable in the presence of length, letter-counting, regular, indexOf, and disequality constraints.
Symbolic computation of differential equivalences
Authors: Cardelli Luca , Tribastone Mirco , Tschaikowski Max , Vandin Andrea
Published: April 2016

Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs. We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. We provide novel symbolic procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories. We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii)~bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. With a prototype implementation we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques.
Environmental bisimulations for probabilistic higher-order languages
Authors: Sangiorgi Davide , Vignudelli Valeria
Published: April 2016

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ- calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as ‘up-to techniques’, are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.
Printing floating-point numbers: a faster, always correct method
Authors: Andrysco Marc , Jhala Ranjit , Lerner Sorin
Published: April 2016

Floating-point numbers are an essential part of modern software, recently gaining particular prominence on the web as the exclusive numeric format of Javascript. To use floating-point numbers, we require a way to convert binary machine representations into human readable decimal outputs. Existing conversion algorithms make trade-offs between completeness and performance. The classic Dragon4 algorithm by Steele and White and its later refinements achieve completeness --- i.e. produce correct and optimal outputs on all inputs --- by using arbitrary precision integer (bignum) arithmetic which leads to a high performance cost. On the other hand, the recent Grisu3 algorithm by Loitsch shows how to recover performance by using native integer arithmetic but sacrifices optimality for 0.5% of all inputs. We present Errol, a new complete algorithm that is guaranteed to produce correct and optimal results for all inputs while simultaneously being 2x faster than the incomplete Grisu3 and 4x faster than previous complete methods.
Newtonian program analysis via tensor product
Authors: Reps Thomas , Turetsky Emma , Prabhu Prathmesh
Published: April 2016

Recently, Esparza et al. generalized Newton's method -- a numerical-analysis algorithm for finding roots of real-valued functions---to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler ``linearized'' problem. One of the reasons this advance is exciting is that some numerical analysts have claimed that ```all' effective and fast iterative [numerical] methods are forms (perhaps very disguised) of Newton's method.'' However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton's method is used on numerical-analysis problems, multiplicative commutativity is relied on to rearrange expressions of the form ``c*X + X*d'' into ``(c+d) * X.'' Such equations correspond to path problems described by regular languages. In contrast, when Newton's method is used for interprocedural dataflow analysis, the ``multiplication'' operation involves function composition, and hence is non-commutative: ``c*X + X*d'' cannot be rearranged into ``(c+d) * X.'' Such equations correspond to path problems described by linear context-free languages (LCFLs). In this paper, we present an improved technique for solving the LCFL sub-problems produced during successive rounds of Newton's method. Our method applies to predicate abstraction, on which most of today's software model checkers rely.
Temporal verification of higher-order functional programs
Authors: Murase Akihiro , Terauchi Tachio , Kobayashi Naoki , Sato Ryosuke , Unno Hiroshi
Published: April 2016

We present an automated approach to verifying arbitrary omega-regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the ``calling relation'' is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.
Transforming spreadsheet data types using examples
Authors: Singh Rishabh , Gulwani Sumit
Published: April 2016

Cleaning spreadsheet data types is a common problem faced by millions of spreadsheet users. Data types such as date, time, name, and units are ubiquitous in spreadsheets, and cleaning transformations on these data types involve parsing and pretty printing their string representations. This presents many challenges to users because cleaning such data requires some background knowledge about the data itself and moreover this data is typically non-uniform, unstructured, and ambiguous. Spreadsheet systems and Programming Languages provide some UI-based and programmatic solutions for this problem but they are either insufficient for the user's needs or are beyond their expertise. In this paper, we present a programming by example methodology of cleaning data types that learns the desired transformation from a few input-output examples. We propose a domain specific language with probabilistic semantics that is parameterized with declarative data type definitions. The probabilistic semantics is based on three key aspects: (i) approximate predicate matching, (ii) joint learning of data type interpretation, and (iii) weighted branches. This probabilistic semantics enables the language to handle non-uniform, unstructured, and ambiguous data. We then present a synthesis algorithm that learns the desired program in this language from a set of input-output examples. We have implemented our algorithm as an Excel add-in and present its successful evaluation on 55 benchmark problems obtained from online help forums and Excel product team.
Abstracting gradual typing
Authors: Garcia Ronald , Clark Alison M. , Tanter Éric
Published: April 2016

Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.
Memoryful geometry of Interaction II: recursion and adequacy
Authors: Muroya Koko , Hoshino Naohiko , Hasuo Ichiro
Published: April 2016

A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the internal states of the latter (called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence ``denotational,'' where transducers are inductively composed using an adaptation of Barbosa's coalgebraic component calculus. In the current paper we extend the mGoI framework and provide a systematic treatment of recursion---an essential feature of programming languages that was however missing in our previous work. Specifically, we introduce two new fixed-point operators in the coalgebraic component calculus. The two follow the previous work on recursion in GoI and are called Girard style and Mackie style: the former obviously exhibits some nice domain-theoretic properties, while the latter allows simpler construction. Their equivalence is established on the categorical (or, traced monoidal) level of abstraction, and is therefore generic with respect to the choice of algebraic effects. Our main result is an adequacy theorem of our mGoI translation, against Plotkin and Power's operational semantics for algebraic effects.
Synthesis of reactive controllers for hybrid systems (keynote)
Authors: Murray Richard M.
Published: April 2016

Decision-making logic in hybrid systems is responsible for selecting modes of operation for the underlying (continuous) control system, reacting to external events and failures in the system, and insuring that the overall control system is satisfying safety and performance specifications. Tools from computer science, such as model-checking and logic synthesis, combined with design patterns from feedback control theory provide new approaches to solving these problems. A major shift is the move from ``design then verify'' to ``specify then synthesize'' approaches to controller design that allow simultaneous synthesis of high-performance, robust control laws and correct-by-construction decision-making logic.
Comparison of the Effects of Dibutyl and Monobutyl Phthalates on the Steroidogenesis of Rat Immature Leydig Cells
Authors: Li Linxi , Chen Xiaomin , Hu Guoxin , Wang Sicong , Xu Renai , Zhu Qiqi , Li Xiaoheng , Wang Mingcang , Lian Qing-Quan , Ge Ren-Shan
Published: April 2016

Dibutyl phthalate (DBP) is a widely used synthetic phthalic diester and monobutyl phthalate (MBP) is its main metabolite. DBP can be released into the environment and potentially disrupting mammalian male reproductive endocrine system. However, the potencies of DBP and MBP to inhibit Leydig cell steroidogenesis and their possible mechanisms are not clear. Immature Leydig cells isolated from rats were cultured with 0.05–50 μM DBP or MBP for 3 h in combination with testosterone synthesis regulator or intermediate. The concentrations of 5α-androstanediol and testosterone in the media were measured, and the mRNA levels of the androgen biosynthetic genes were detected by qPCR. The direct actions of DBP or MBP on CYP11A1, CYP17A1, SRD5A1, and AKR1C14 activities were measured. MBP inhibited androgen production by the immature Leydig cell at as low as 50 nM, while 50 μM was required for DBP to suppress its androgen production. MBP mainly downregulatedCyp11a1andHsd3b1expression levels at 50 nM. However, 50 μM DBP downregulatedStar,Hsd3b1, andHsd17b3expression levels and directly inhibited CYP11A1 and CYP17A1 activities. In conclusion, DBP is metabolized to more potent inhibitor MBP that downregulated the expression levels of some androgen biosynthetic enzymes.
Sorption Profile of Phosphorus Ions onto ZnO Nanorods Synthesized via Sonic Technique
Authors: Elkady M. F. , Shokry Hassan H. , Salama Eslam
Published: April 2016

High surface area zinc oxide material in nanorod morphological structure was synthesized using an ultrasonic technique in the presence of polyvinyl pyrrolidone as stabilizing agent. The crystallite, morphology, and surface area of the prepared white powder material were identified using XRD, SEM, and BET techniques, respectively. X-ray analysis confirms the high purity of synthesized ZnO. The evaluated specific surface area of prepared ZnO was 16.7 m2/g; this value guarantees high efficiency for water purification. The feasibility of synthesized ZnO nanorods for phosphorus sorption from aqueous solution was established using batch technique. Nano-zinc oxide exhibits high efficiency for phosphorus removal; the equilibrium state was recorded within 90 minutes. The most effective hydrogen ion concentration of the polluted solution was recorded at pH = 1 for phosphorus decontamination. The equilibrium of phosphorus sorption onto ZnO nanorods was well explained using both Langmuir and Temkin isotherm models. The calculated maximum monolayer sorption capacity was 89 mg/g according to Langmuir isotherm at 27°C. In order to explain the phosphorus sorption mechanism onto the prepared ZnO nanorods, three simplified kinetic models of pseudo-first order, pseudo-second order, and intraparticle diffusion rate models were tested. Kinetics was well fitted by pseudo-second order kinetic model with a contribution of intraparticle diffusion.
Pneumothorax Caused by an Isolated Midshaft Clavicle Fracture
Authors: Feriani Najla , Ben Ghezala Hassen , Snouda Salah
Published: April 2016

Patients with isolated clavicle fractures are frequent in the emergency department. However, unusual clavicle fractures complications, such as pneumothorax, are rare. Previous reports indicated that all pneumothorax cases were treated via performing thoracostomy. Conservatively, the treatment of the clavicle fracture, like in our case, was successful. Despite the fact that isolated clavicle fractures rarely cause complications and generally heal with immobilization, serious complications may occur requiring urgent treatment. It has been proven that physical examinations, with particular attention to the neurovascular and chest examinations, and radiographs of the clavicle are necessary to prevent overlooking these potentially dangerous complications.
A Novel Improved Probability-Guided RANSAC Algorithm for Robot 3D Map Building
Authors: Jia Songmin , Wang Ke , Li Xiuzhi , Xu Tao
Published: April 2016

This paper presents a novel improved RANSAC algorithm based on probability and DS evidence theory to deal with the robust pose estimation in robot 3D map building. In this proposed RANSAC algorithm, a parameter model is estimated by using a random sampling test set. Based on this estimated model, all points are tested to evaluate the fitness of current parameter model and their probabilities are updated by using a total probability formula during the iterations. The maximum size of inlier set containing the test point is taken into account to get a more reliable evaluation for test points by using DS evidence theory. Furthermore, the theories of forgetting are utilized to filter out the unstable inliers and improve the stability of the proposed algorithm. In order to boost a high performance, an inverse mapping sampling strategy is adopted based on the updated probabilities of points. Both the simulations and real experimental results demonstrate the feasibility and effectiveness of the proposed algorithm.
AC Humidity Sensing Properties of Mesoporous K2CO3-SiO2Composite Materials
Authors: Guo Liang , Chu Xuefeng , Gao Xiaohong , Wang Chao , Chi Yaodan , Yang Xiaotian
Published: April 2016

The mesoporous silica SBA-15 and mesoporous K2CO3-SiO2composite material were synthesized. Characterization of microstructure and morphology of materials indicated that the composite material had saved the porous framework of mesoporous silica SBA-15. Humidity sensing properties of different inverse proportion K2CO3-SiO2composite material were studied and we found that the sample with 0.16 g/g K2CO3exhibited excellent linearity in the wide humidity range. The complex impedance changed five orders of magnitude from 11% RH to 95% RH. The rapid response and recovery time were 10 s and 38 s, respectively. Finally a feasible ion transfer mechanism was brought forward to explain the sensing mechanism.
Progenitor Hematopoietic Cells Implantation Improves Functional Capacity of End Stage Coronary Artery Disease Patients with Advanced Heart Failure
Authors: Yuniadi Yoga , Kusnadi Yuyus , Sandhow Lakshmi , Erika Rendra , Hanafy Dicky A. , Sardjono Caroline , Kaligis R. W. M. , Kasim Manoefris , Harimurti Ganesja M.
Published: April 2016

Background. Proangiogenic Hematopoietic Cells (PHC) which comprise diverse mixture of cell types are able to secrete proangiogenic factors and interesting candidate for cell therapy. The aim of this study was to seek for benefit in implantation of PHC on functional improvement in end stage coronary artery disease patients with advanced heart failure.Methods. Patients with symptomatic heart failure despite guideline directed medical therapy and LVEF less than 35% were included. Peripheral blood mononuclear cells were isolated, cultivated for 5 days, and then harvested. Flow cytometry and cell surface markers were used to characterize PHC. The PHC were delivered retrogradely via sinus coronarius. Echocardiography, myocardial perfusion, and clinical and functional data were analyzed up to 1-year observation.Results. Of 30 patients (56.4±7.40 yo) preimplant NT proBNP level is5124.5±4682.50 pmol/L. Harvested cells characterized with CD133, CD34, CD45, and KDR showed0.87±0.41,0.63±0.66,99.00±2.60, and3.22±3.79%, respectively. LVEF was improved (22±5.68versus26.8±7.93,p<0.001) during short and long term observation. Myocardial perfusion significantly improved 6 months after treatment. NYHA Class and six-minute walk test are improved during short term and long term follow-up.Conclusion. Expanded peripheral blood PHC implantation using retrograde delivery approach improved LV systolic function, myocardial perfusion, and functional capacity.
Paraoxonase-1 and Simvastatin Treatment in Patients with Stable Coronary Artery Disease
Authors: Januszek Rafał
Published: April 2016

Background.Paraoxonase-1 (PON1) is the crucial antioxidant marker of high-density lipoproteins. The present study is aimed at assessing the effect of simvastatin treatment on PON1 activity and its relationship to Q192R and M55L polymorphisms in subjects with stable coronary artery disease (CAD).Methods.The patient group was composed of 53 individuals with stable CAD, and the control group included 53 sex-matched police officers without CAD. CAD patients were treated with simvastatin 40mg/day for 12 months. Respectively, flow mediated dilatation (FMD), serum hs-CRP and TNF-αlevels, urinary 8-iso-PGF2αconcentrations, and PON1 activity were evaluated in definitive intervals.Results.There was no effect of simvastatin treatment on urinary 8-iso-PGF2α. Simvastatin treatment significantly increased FMD value, decreased CRP and TNF-αconcentration. After adjusting for PON1 genotypes, significantly higher PON1 activity was noted in the 192R allele carriers, in both groups. Regardless of genotype, PON1 activity remained stable after simvastatin treatment.Conclusions.The present study confirms a positive effect of simvastatin therapy on endothelial function and inflammatory markers in secondary prevention. Simvastatin treatment shows no effects on PON1 activity and 8-isoprostanes level. The effect of simvastatin therapy on PON1 activity is not modulated by Q192R and M55L polymorphisms.
WWOX CNV-67048 Functions as a Risk Factor for Epithelial Ovarian Cancer in Chinese Women by Negatively Interacting with Oral Contraceptive Use
Authors: Chen Yongxiu , Tan Xiaochang , Ding Yongli , Mai Bi , Huang Xiaowen , Hu Guiying , Luo Xiping
Published: April 2016

Copy number variations (CNVs) have attracted increasing evidences to represent their roles as cancer susceptibility regulators. However, little is known about the role of CNV in epithelia ovarian cancer (EOC). Recently, the CNV-67048 of WW domain-containing oxidoreductase (WWOX) was reported to alter cancer risks. Considering thatWWOXalso plays a role in EOC, we hypothesized that the CNV-67048 was associated with EOC risk. In a case-control study of 549 EOC patients and 571 age (±5 years) matched cancer-free controls, we found that the low copy number of CNV-67048 (1-copy and 0-copy) conferred a significantly increased risk of EOC (OR = 1.346, 95% CI = 1.037–1.747) and it determined the risk by means of copy number-dependent dosage effect (P=0.009). Data from TCGA also confirmed the abovementioned association as the frequency of low copies in EOC group was 3.68 times more than that in healthy group (P=0.023). The CNV also negatively interacted with oral contraceptive use on EOC risk (P=0.042). Functional analyses further showed a lower mRNA level of WWOX in tissues with the 0-copy or 1-copy than that in those with the 2-copy (P=0.045). Our data suggested the CNV-67048 to be a risk factor of EOC in Chinese women.
Paraneoplastic Pemphigus Associated with Follicular Dendritic Cell Tumor in the Mediastinum
Authors: Prakasan Aparna Mullangath , Prabhu Anne Jennifer , Velarasan Kanmani , Backianathan Selvamani , Ram Thomas Samuel
Published: April 2016

Paraneoplastic Pemphigus (PNP) is an autoimmune bullous disease characterized by severe stomatitis, polymorphous skin eruptions, and underlying neoplasms. Diagnosis of cutaneous paraneoplastic disorders requires high index of suspicion. We describe a patient with PNP associated with follicular dendritic cell (FDC) tumor in the mediastinum, a rare neoplasm originating from follicular dendritic cells. Its management requires identification of underlying malignancy and treatment of the same. Our patient showed remission of PNP upon excision of the tumor and remained disease-free for 8 years.