bluuebunny/crossref_metadata_2025 huggingface dataset:
Semantic subtyping for imperative object-oriented languages
Authors: Ancona Davide , Corradi Andrea
Published: December 2016

Semantic subtyping is an approach for defining sound and complete procedures to decide subtyping for expressive types, including union and intersection types; although it has been exploited especially in functional languages for XML based programming, recently it has been partially investigated in the context of object-oriented languages, and a sound and complete subtyping algorithm has been proposed for record types, but restricted to immutable fields, with union and recursive types interpreted coinductively to support cyclic objects. In this work we address the problem of studying semantic subtyping for imperative object-oriented languages, where fields can be mutable; in particular, we add read/write field annotations to record types, and, besides union, we consider intersection types as well, while maintaining coinductive interpretation of recursive types. In this way, we get a richer notion of type with a flexible subtyping relation, able to express a variety of type invariants useful for enforcing static guarantees for mutable objects. The addition of these features radically changes the defi- nition of subtyping, and, hence, the corresponding decision procedure, and surprisingly invalidates some subtyping laws that hold in the functional setting. We propose an intuitive model where mutable record val- ues contain type information to specify the values that can be correctly stored in fields. Such a model, and the correspond- ing subtyping rules, require particular care to avoid circularity between coinductive judgments and their negations which, by duality, have to be interpreted inductively. A sound and complete subtyping algorithm is provided, together with a prototype implementation.
Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations
Authors: Itzhaky Shachar , Singh Rohit , Solar-Lezama Armando , Yessenov Kuat , Lu Yongquan , Leiserson Charles , Chowdhury Rezaul
Published: December 2016

We introduce a framework allowing domain experts to manipulate computational terms in the interest of deriving better, more efficient implementations.It employs deductive reasoning to generate provably correct efficient implementations from a very high-level specification of an algorithm, and inductive constraint-based synthesis to improve automation. Semantic information is encoded into program terms through the use of refinement types.

In this paper, we develop the technique in the context of a system called Bellmania that uses solver-aided tactics to derive parallel divide-and-conquer implementations of dynamic programming algorithms that have better locality and are significantly more efficient than traditional loop-based implementations. Bellmania includes a high-level language for specifying dynamic programming algorithms and a calculus that facilitates gradual transformation of these specifications into efficient implementations. These transformations formalize the divide-and conquer technique; a visualization interface helps users to interactively guide the process, while an SMT-based back-end verifies each step and takes care of low-level reasoning required for parallelism.

We have used the system to generate provably correct implementations of several algorithms, including some important algorithms from computational biology, and show that the performance is comparable to that of the best manually optimized code.
A practical framework for type inference error explanation
Authors: Loncaric Calvin , Chandra Satish , Schlesinger Cole , Sridharan Manu
Published: December 2016

Many languages have support for automatic type inference. But when inference fails, the reported error messages can be unhelpful, highlighting a code location far from the source of the problem. Several lines of work have emerged proposing error reports derived from correcting sets: a set of program points that, when fixed, produce a well-typed program. Unfortunately, these approaches are tightly tied to specific languages; targeting a new language requires encoding a type inference algorithm for the language in a custom constraint system specific to the error reporting tool.

We show how to produce correcting set-based error reports by leveraging existing type inference implementations, easing the burden of adoption and, as type inference algorithms tend to be efficient in practice, producing error reports of comparable quality to similar error reporting tools orders of magnitude faster. Many type inference algorithms are already formulated as dual phases of type constraint generation and solving; rather than (re)implementing type inference in an error explanation tool, we isolate the solving phase and treat it as an oracle for solving typing constraints. Given any set of typing constraints, error explanation proceeds by iteratively removing conflicting constraints from the initial constraint set until discovering a subset on which the solver succeeds; the constraints removed form a correcting set. Our approach is agnostic to the semantics of any particular language or type system, instead leveraging the existing type inference engine to give meaning to constraints.
The missing link: explaining ELF static linking, semantically
Authors: Kell Stephen , Mulligan Dominic P. , Sewell Peter
Published: December 2016

Beneath the surface, software usually depends on complex
linker behaviour
to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as libc and operating system kernels rely on a host of linker features. But linking is poorly understood by working programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and the poorly specified
linker speak
by which they are controlled: metadata in object files, command-line options, and linker-script language. We provide the first validated formalisation of a realistic executable and linkable format (ELF), and capture aspects of the Application Binary Interfaces for four mainstream platforms (AArch64, AMD64, Power64, and IA32). Using these, we develop an executable specification of static linking, covering (among other things) enough to link small C programs (we use the example of bzip2) into a correctly running executable. We provide our specification in Lem and Isabelle/HOL forms. This is the first formal specification of mainstream linking. We have used the Isabelle/HOL version to prove a sample correctness property for one case of AMD64 ABI relocation, demonstrating that the specification supports formal proof, and as a first step towards the much more ambitious goal of verified linking. Our work should enable several novel strands of research, including linker-aware verified compilation and program analysis, and better languages for controlling linking.
Efficient and thread-safe objects for dynamically-typed languages
Authors: Daloze Benoit , Marr Stefan , Bonetta Daniele , Mössenböck Hanspeter
Published: December 2016

We are in the multi-core era. Dynamically-typed languages are in widespread use, but their support for multithreading still lags behind. One of the reasons is that the sophisticated techniques they use to efficiently represent their dynamic object models are often unsafe in multithreaded environments.

This paper defines safety requirements for dynamic object models in multithreaded environments. Based on these requirements, a language-agnostic and thread-safe object model is designed that maintains the efficiency of sequential approaches. This is achieved by ensuring that field reads do not require synchronization and field updates only need to synchronize on objects shared between threads.

Basing our work on JRuby+Truffle, we show that our safe object model has zero overhead on peak performance for thread-local objects and only 3% average overhead on parallel benchmarks where field updates require synchronization. Thus, it can be a foundation for safe and efficient multithreaded VMs for a wide range of dynamic languages.
An improved algorithm for slicing machine code
Authors: Srinivasan Venkatesh , Reps Thomas
Published: December 2016

Machine-code slicing is an important primitive for building binary analysis and rewriting tools, such as taint trackers, fault localizers, and partial evaluators. However, it is not easy to create a machine-code slicer that exhibits a high level of precision. Moreover, the problem of creating such a tool is compounded by the fact that a small amount of local imprecision can be amplified via cascade effects.

Most instructions in instruction sets such as Intel's IA-32 and ARM are multi-assignments: they have several inputs and several outputs (registers, flags, and memory locations). This aspect of the instruction set introduces a granularity issue during slicing: there are often instructions at which we would like the slice to include only a subset of the instruction's semantics, whereas the slice is forced to include the entire instruction. Consequently, the slice computed by state-of-the-art tools is very imprecise, often including essentially the entire program.

This paper presents an algorithm to slice machine code more accurately. To counter the granularity issue, our algorithm performs slicing at the microcode level, instead of the instruction level, and obtains a more precise microcode slice. To reconstitute a machine-code program from a microcode slice, our algorithm uses machine-code synthesis. Our experiments on IA-32 binaries of FreeBSD utilities show that, in comparison to slices computed by a state-of-the-art tool, our algorithm reduces the size of backward slices by 33%, and forward slices by 70%.
Speeding up machine-code synthesis
Authors: Srinivasan Venkatesh , Sharma Tushar , Reps Thomas
Published: December 2016

Machine-code synthesis is the problem of searching for an instruction sequence that implements a semantic specification, given as a formula in quantifier-free bit-vector logic (QFBV). Instruction sets like Intel's IA-32 have around 43,000 unique instruction schemas; this huge instruction pool, along with the exponential cost inherent in enumerative synthesis, results in an enormous search space for a machine-code synthesizer: even for relatively small specifications, the synthesizer might take several hours or days to find an implementation. In this paper, we present several improvements to the algorithms used in a state-of-the-art machine-code synthesizer McSynth. In addition to a novel pruning heuristic, our improvements incorporate a number of ideas known from the literature, which we adapt in novel ways for the purpose of speeding up machine-code synthesis. Our experiments for Intel's IA-32 instruction set show that our improvements enable synthesis of code for 12 out of 14 formulas on which McSynth times out, speeding up the synthesis time by at least 1981X, and for the remaining formulas, speeds up synthesis by 3X.
Type soundness for dependent object types (DOT)
Authors: Rompf Tiark , Amin Nada
Published: December 2016

Scala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for restricted subsets of DOT. In fact, it has been shown that important Scala features such as type refinement or a subtyping relation with lattice structure break at least one key metatheoretic property such as environment narrowing or invertible subtyping transitivity, which are usually required for a type soundness proof. The main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a rich DOT calculus that includes recursive type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that subtyping transitivity only needs to be invertible in code paths executed at runtime, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.
Automated reasoning for web page layout
Authors: Panchekha Pavel , Torlak Emina
Published: December 2016

Web pages define their appearance using Cascading Style Sheets, a modular language for layout of tree-structured documents. In principle, using CSS is easy: the developer specifies declarative constraints on the layout of an HTML document (such as the positioning of nodes in the HTML tree), and the browser solves the constraints to produce a box-based rendering of that document. In practice, however, the subtleties of CSS semantics make it difficult to develop stylesheets that produce the intended layout across different user preferences and browser settings.

This paper presents the first mechanized formalization of a substantial fragment of the CSS semantics. This formalization is equipped with an efficient reduction to the theory of quantifier-free linear real arithmetic, enabling effective automated reasoning about CSS stylesheets and their behavior. We implement this reduction in Cassius, a solver-aided framework for building semantics-aware tools for CSS. To demonstrate the utility of Cassius, we prototype new tools for automated verification, debugging, and synthesis of CSS code. We show that these tools work on fragments of real-world websites, and that Cassius is a practical first step toward solver-aided programming for the web.
Finding resume and restart errors in Android applications
Authors: Shan Zhiyong , Azim Tanzirul , Neamtiu Iulian
Published: December 2016

Smartphone apps create and handle a large variety of ``instance'' data that has to persist across runs, such as the current navigation route, workout results, antivirus settings, or game state. Due to the nature of the smartphone platform, an app can be paused, sent into background, or killed at any time. If the instance data is not saved and restored between runs, in addition to data loss, partially-saved or corrupted data can crash the app upon resume or restart. While smartphone platforms offer API support for data-saving and data-retrieving operations, the use of this API is ad-hoc: left to the programmer, rather than enforced by the compiler. We have observed that several categories of bugs---including data loss, failure to resume/restart or resuming/restarting in the wrong state---are due to incorrect handling of instance data and are easily triggered by just pressing the `Home' or `Back' buttons. To help address this problem, we have constructed a tool chain for Android (the KREfinder static analysis and the KREreproducer input generator) that helps find and reproduce such incorrect handling. We have evaluated our approach by running the static analysis on 324 apps, of which 49 were further analyzed manually. Results indicate that our approach is (i) effective, as it has discovered 49 bugs, including in popular Android apps, and (ii) efficient, completing on average in 61 seconds per app. More generally, our approach helps determine whether an app saves too much or too little state.
Scalable verification of border gateway protocol configurations with an SMT solver
Authors: Weitz Konstantin , Woos Doug , Torlak Emina , Ernst Michael D. , Krishnamurthy Arvind , Tatlock Zachary
Published: December 2016

Internet Service Providers (ISPs) use the Border Gateway Protocol (BGP) to announce and exchange routes for de- livering packets through the internet. ISPs must carefully configure their BGP routers to ensure traffic is routed reli- ably and securely. Correctly configuring BGP routers has proven challenging in practice, and misconfiguration has led to worldwide outages and traffic hijacks. This paper presents Bagpipe, a system that enables ISPs to declaratively express BGP policies and that automatically verifies that router configurations implement such policies. The novel initial network reduction soundly reduces policy verification to a search for counterexamples in a finite space. An SMT-based symbolic execution engine performs this search efficiently. Bagpipe reduces the size of its search space using predicate abstraction and parallelizes its search using symbolic variable hoisting. Bagpipe's policy specification language is expressive: we expressed policies inferred from real AS configurations, policies from the literature, and policies for 10 Juniper TechLibrary configuration scenarios. Bagpipe is efficient: we ran it on three ASes with a total of over 240,000 lines of Cisco and Juniper BGP configuration. Bagpipe is effective: it revealed 19 policy violations without issuing any false positives.
Parallel incremental whole-program optimizations for Scala.js
Authors: Doeraene Sébastien , Schlatter Tobias
Published: December 2016

Whole-program optimizations are powerful tools that can dramatically improve performance, size and other aspects of programs. Because they depend on global knowledge, they must typically be reapplied to the whole program when small changes are made, which makes them too slow for the development cycle. This is an issue for some environments that require, or benefit a lot from, whole-program optimizations, such as compilation to JavaScript or to the Dalvik VM, because their development cycle is slowed down either by the lack of optimizations, or by the time spent on applying them.

We present a new approach to designing incremental whole-program optimizers for object-oriented and functional languages: when part of a program changes, only the portions affected by the changes are reoptimized. An incremental optimizer using this approach for Scala.js, the Scala to JavaScript compiler, demonstrates speedups from 10x to 100x compared to its batch version. As a result, the optimizer's running time becomes insignificant compared to separate compilation, making it fit for use on every compilation run during the development cycle. We also show how to parallelize the incremental algorithm to take advantage of multicore hardware.
To be precise: regression aware debugging
Authors: Bavishi Rohan , Pandey Awanish , Roy Subhajit
Published: December 2016

Bounded model checking based debugging solutions search for mutations of program expressions that produce the expected output for a currently failing test. However, the current localization tools are not
regression aware
: they do not use information from the passing tests in their localization formula. On the other hand, the current repair tools attempt to guarantee
regression freedom
: when provided with a set of passing tests, they guarantee that none of these tests can break due to the suggested repair patch, thereby constructing a large repair formula.

In this paper, we propose
regression awareness
as a means to improve the quality of localization and to scale repair. To enable regression awareness, we summarize the proof of correctness of each passing test by computing Craig Interpolants over a symbolic encoding of the passing execution, and use these summaries as additional soft constraints while synthesizing altered executions corresponding to failing tests. Intuitively, these additional constraints act as roadblocks, thereby discouraging executions that may damage the proof of a passing test. We use a partial MAXSAT solver to relax the proofs in a systematic way, and use a ranking function that penalizes mutations that damage the existing proofs.

We have implemented our algorithms into a tool, TINTIN, that enables
regression aware
localization and repair. For localizations, our strategy is effective in extracting a superior ranking of suspicious locations: on a set of 52 different versions across 12 different programs spanning three benchmark suites, TINTIN achieves a saving of developer effort by almost 45% (in terms of the locations that must be examined by a developer to reach the ground-truth repair) in the worst case and 27% in the average case over existing techniques. For automated repairs, on our set of benchmarks, TINTIN achieves a 2.3X speedup over existing techniques without sacrificing much on the ranking of the repair patches: the ground-truth repair appears as the topmost suggestion in more than 70% of our benchmarks.
Type inference for static compilation of JavaScript
Authors: Chandra Satish , Gordon Colin S. , Jeannin Jean-Baptiste , Schlesinger Cole , Sridharan Manu , Tip Frank , Choi Youngil
Published: December 2016

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.
Purposes, concepts, misfits, and a redesign of git
Authors: De Rosso Santiago Perez , Jackson Daniel
Published: December 2016

Git is a widely used version control system that is powerful but complicated. Its complexity may not be an inevitable consequence of its power but rather evidence of flaws in its design. To explore this hypothesis, we analyzed the design of Git using a theory that identifies concepts, purposes, and misfits. Some well-known difficulties with Git are described, and explained as misfits in which underlying concepts fail to meet their intended purpose. Based on this analysis, we designed a reworking of Git (called Gitless) that attempts to remedy these flaws.

To correlate misfits with issues reported by users, we conducted a study of Stack Overflow questions. And to determine whether users experienced fewer complications using Gitless in place of Git, we conducted a small user study. Results suggest our approach can be profitable in identifying, analyzing, and fixing design problems.
Ringer: web automation by demonstration
Authors: Barman Shaon , Chasins Sarah , Bodik Rastislav , Gulwani Sumit
Published: December 2016

With increasing amounts of data available on the web and a diverse range of users interested in programmatically accessing that data, web automation must become easier. Automation helps users complete many tedious interactions, such as scraping data, completing forms, or transferring data between websites. However, writing web automation scripts typically requires an expert programmer because the writer must be able to reverse engineer the target webpage. We have built a record and replay tool, Ringer, that makes web automation accessible to non-coders. Ringer takes a user demonstration as input and creates a script that interacts with the page as a user would. This approach makes Ringer scripts more robust to webpage changes because user-facing interfaces remain relatively stable compared to the underlying webpage implementations. We evaluated our approach on benchmarks recorded on real webpages and found that it replayed 4x more benchmarks than a state-of-the-art replay tool.
Accelerating program analyses by cross-program training
Authors: Kulkarni Sulekha , Mangal Ravi , Zhang Xin , Naik Mayur
Published: December 2016

Practical programs share large modules of code. However, many program analyses are ineffective at reusing analysis results for shared code across programs. We present POLYMER, an analysis optimizer to address this problem. POLYMER runs the analysis offline on a corpus of training programs and learns analysis facts over shared code. It prunes the learnt facts to eliminate intermediate computations and then reuses these pruned facts to accelerate the analysis of other programs that share code with the training corpus. We have implemented POLYMER to accelerate analyses specified in Datalog, and apply it to optimize two analyses for Java programs: a call-graph analysis that is flow- and context-insensitive, and a points-to analysis that is flow- and context-sensitive. We evaluate the resulting analyses on ten programs from the DaCapo suite that share the JDK library. POLYMER achieves average speedups of 2.6× for the call- graph analysis and 5.2× for the points-to analysis.
FIDEX: filtering spreadsheet data using examples
Authors: Wang Xinyu , Gulwani Sumit , Singh Rishabh
Published: December 2016

Data filtering in spreadsheets is a common problem faced by millions of end-users. The task of data filtering requires a computational model that can separate intended positive and negative string instances. We present a system, FIDEX, that can efficiently learn desired data filtering expressions from a small set of positive and negative string examples.

There are two key ideas of our approach. First, we design an expressive DSL to represent disjunctive filter expressions needed for several real-world data filtering tasks. Second, we develop an efficient synthesis algorithm for incrementally learning consistent filter expressions in the DSL from very few positive and negative examples. A DAG-based data structure is used to succinctly represent a large number of filter expressions, and two corresponding operators are defined for algorithmically handling positive and negative examples, namely, the intersection and subtraction operators. FIDEX is able to learn data filters for 452 out of 460 real-world data filtering tasks in real time (0.22s), using only 2.2 positive string instances and 2.7 negative string instances on average.
Apex: automatic programming assignment error explanation
Authors: Kim Dohyeong , Kwon Yonghwi , Liu Peng , Kim I. Luk , Perry David Mitchel , Zhang Xiangyu , Rodriguez-Rivera Gustavo
Published: December 2016

This paper presents Apex, a system that can automatically generate explanations for programming assignment bugs, regarding where the bugs are and how the root causes led to the runtime failures. It works by comparing the passing execution of a correct implementation (provided by the instructor) and the failing execution of the buggy implementation (submitted by the student). The technique overcomes a number of technical challenges caused by syntactic and semantic differences of the two implementations. It collects the symbolic traces of the executions and matches assignment statements in the two execution traces by reasoning about symbolic equivalence. It then matches predicates by aligning the control dependences of the matched assignment statements, avoiding direct matching of path conditions which are usually quite different. Our evaluation shows that Apex is every effective for 205 buggy real world student submissions of 4 programming assignments, and a set of 15 programming assignment type of buggy programs collected from stackoverflow.com, precisely pinpointing the root causes and capturing the causality for 94.5% of them. The evaluation on a standard benchmark set with over 700 student bugs shows similar results. A user study in the classroom shows that Apex has substantially improved student productivity.
Stateless model checking with data-race preemption points
Authors: Blum Ben , Gibson Garth
Published: December 2016

Stateless model checking is a powerful technique for testing concurrent programs, but suffers from exponential state space explosion when the test input parameters are too large. Several reduction techniques can mitigate this explosion, but even after pruning equivalent interleavings, the state space size is often intractable. Most prior tools are limited to preempting only on synchronization APIs, which reduces the space further, but can miss unsynchronized thread communication bugs. Data race detection, another concurrency testing approach, focuses on suspicious memory access pairs during a single test execution. It avoids concerns of state space size, but may report races that do not lead to observable failures, which jeopardizes a user’s willingness to use the analysis.

We present Quicksand, a new stateless model checking framework which manages the exploration of many state spaces using different preemption points. It uses state space estimation to prioritize jobs most likely to complete in a fixed CPU budget, and it incorporates data-race analysis to add new preemption points on the fly. Preempting threads during a data race’s instructions can automatically classify the race as buggy or benign, and uncovers new bugs not reachable by prior model checkers. It also enables full verification of all possible schedules when every data race is verified as benign within the CPU budget. In our evaluation, Quicksand found 1.25x as many bugs and verified 4.3x as many tests compared to prior model checking approaches.
First-class effect reflection for effect-guided programming
Authors: Long Yuheng , Liu Yu David , Rajan Hridesh
Published: December 2016

This paper introduces a novel type-and-effect calculus, first-class effects, where the computational effect of an expression can be programmatically reflected, passed around as values, and analyzed at run time. A broad range of designs "hard-coded" in existing effect-guided analyses — from thread scheduling, version-consistent software updating, to data zeroing — can be naturally supported through the programming abstractions. The core technical development is a type system with a number of features, including a hybrid type system that integrates static and dynamic effect analyses, a refinement type system to verify application-specific effect management properties, a double-bounded type system that computes both over-approximation of effects and their under-approximation. We introduce and establish a notion of soundness called trace consistency, defined in terms of how the effect and trace correspond. The property sheds foundational insight on "good" first-class effect programming.
GEMs: shared-memory parallel programming for Node.js
Authors: Bonetta Daniele , Salucci Luca , Marr Stefan , Binder Walter
Published: December 2016

JavaScript is the most popular programming language for client-side Web applications, and Node.js has popularized the language for server-side computing, too. In this domain, the minimal support for parallel programming remains however a major limitation. In this paper we introduce a novel parallel programming abstraction called
Generic Messages
(GEMs). GEMs allow one to combine message passing and shared-memory parallelism, extending the classes of parallel applications that can be built with Node.js. GEMs have customizable semantics and enable several forms of thread safety, isolation, and concurrency control. GEMs are designed as convenient JavaScript abstractions that expose high-level and safe parallelism models to the developer. Experiments show that GEMs outperform equivalent Node.js applications thanks to their usage of shared memory.
LaCasa: lightweight affinity and object capabilities in Scala
Authors: Haller Philipp , Loiko Alex
Published: December 2016

Aliasing is a known source of challenges in the context of imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show promise, they do not address the need of aliasing control in existing languages.

This paper presents a new approach to isolation and uniqueness in an existing, widely-used language, Scala. The approach is unique in the way it addresses some of the most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code requires only a minimal set of annotations. Only a single bit of information is required per class. Surprisingly, the paper shows that this information can be provided by the object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove key soundness theorems. The type system is implemented for the full Scala language, providing, for the first time, a sound integration with Scala's local type inference. Finally, we empirically evaluate the conformity of existing Scala open-source code on a corpus of over 75,000 LOC.
Role of autonomic nervous system in chronic CNS-mediated antidiabetic action of leptin
Authors: da Silva Alexandre A. , Hall John E. , Moak Sydney P. , Browning Jackson , Houghton Haley J. , Micheloni Giovana C. , do Carmo Jussara M.
Published: December 2016

This study tested whether ganglionic blockade or hepatic vagotomy attenuates the chronic central nervous system (CNS)-mediated antidiabetic and cardiovascular effects of leptin. Male Sprague-Dawley rats were instrumented with telemetry probes and arterial and venous catheters for determination of blood pressure (BP), heart rate (HR), blood sampling, and intravenous (iv) infusions. An intracerebroventricular (ICV) cannula was placed into the brain lateral ventricle for infusion of leptin or vehicle. After control measurements, streptozotocin (STZ) was injected iv (50 mg/kg) to induce diabetes, and 5 days later leptin ( n = 6) or saline vehicle ( n = 5) was infused ICV for 12 days via osmotic pumps. Beginning on day 6 of leptin treatment, the ganglionic blocker hexamethonium (15 mg·kg−1·day−1 iv) was infused, while leptin infusion was continued, to assess the role of the autonomic nervous system. Induction of diabetes was associated with increases in blood glucose (98 ± 7 to 350 ± 19 mg/dl), food intake (23 ± 3 to 43 ± 3 g/day), decreases in HR (−70 ± 11 beats/min), polyuria, and increased water consumption, which were all completely normalized by ICV leptin infusion. Although hexamethonium attenuated leptin’s effect on HR, it failed to impair leptin’s ability to restore euglycemia or to prevent the polyuria or increased water intake in STZ-diabetic rats. We also found that after pretreatment with hexamethonium ( n = 8), ICV leptin infusion, during continued ganglionic blockade, completely normalized blood glucose in diabetic rats. In addition, selective hepatic vagotomy did not attenuate leptin’s ability to restore euglycemia in diabetic rats. These results suggest that leptin’s powerful chronic CNS antidiabetic actions are mediated primarily via nonautonomic mechanisms.
Type of supplemented simple sugar, not merely calorie intake, determines adverse effects on metabolism and aortic function in female rats
Authors: Sangüesa Gemma , Shaligram Sonali , Akther Farjana , Roglans Núria , Laguna Juan C. , Rahimian Roshanak , Alegret Marta
Published: December 2016

High consumption of simple sugars causes adverse cardiometabolic effects. We investigated the mechanisms underlying the metabolic and vascular effects of glucose or fructose intake and determined whether these effects are exclusively related to increased calorie consumption. Female Sprague-Dawley rats were supplemented with 20% wt/vol glucose or fructose for 2 mo, and plasma analytes and aortic response to vasodilator and vasoconstrictor agents were determined. Expression of molecules associated with lipid metabolism, insulin signaling, and vascular response were evaluated in hepatic and/or aortic tissues. Caloric intake was increased in both sugar-supplemented groups vs. control and in glucose- vs. fructose-supplemented rats. Hepatic lipogenesis was induced in both groups. Plasma triglycerides were increased only in the fructose group, together with decreased expression of carnitine palmitoyltransferase-1A and increased microsomal triglyceride transfer protein expression in the liver. Plasma adiponectin and peroxisome proliferator-activated receptor (PPAR)-α expression was increased only by glucose supplementation. Insulin signaling in liver and aorta was impaired in both sugar-supplemented groups, but the effect was more pronounced in the fructose group. Fructose supplementation attenuated aortic relaxation response to a nitric oxide (NO) donor, whereas glucose potentiated it. Phenylephrine-induced maximal contractions were reduced in the glucose group, which could be related to increased endothelial NO synthase (eNOS) phosphorylation and subsequent elevated basal NO in the glucose group. In conclusion, despite higher caloric intake in glucose-supplemented rats, fructose caused worse metabolic and vascular responses. This may be because of the elevated adiponectin level and the subsequent enhancement of PPARα and eNOS phosphorylation in glucose-supplemented rats.

NEW & NOTEWORTHY This is the first study comparing the effects of glucose and fructose consumption on metabolic factors and aortic function in female rats. Our results show that, although total caloric consumption was higher in glucose-supplemented rats, fructose ingestion had a greater impact in inducing metabolic and aortic dysfunction.
Bothrops jararaca and Bothrops erythromelas Snake Venoms Promote Cell Cycle Arrest and Induce Apoptosis via the Mitochondrial Depolarization of Cervical Cancer Cells
Authors: Bernardes-Oliveira Emanuelly , Gomes Dayanne Lopes , Martelli Palomino Gustavo , Juvenal Silva Farias Kleber , da Silva Wilmar Dias , Rocha Hugo Alexandre Oliveira , Gonçalves Ana Katherine , Fernandes-Pedrosa Matheus de Freitas , Crispim Janaina Cristiana de Oliveira
Published: December 2016

Bothrops jararaca (BJ) and Bothrops erythromelas (BE) are viper snakes found in South‐Southeast and Northeast regions of Brazil, respectively. Snake venoms are bioactive neurotoxic substances synthesized and stored by venom glands, with different physiological and pharmacological effects, recently suggesting a possible preference for targets in cancer cells; however, mechanisms of snakes have been little studied. Here, we investigated the mechanism responsible for snake crude venoms toxicity in cultured cervical cancer cells SiHa and HeLa. We show that BJ and BE snake crude venoms exert cytotoxic effects to these cells. The percentage of apoptotic cells and cell cycle analysis and cell proliferation were assessed by flow cytometry and MTT assay. Detection of mitochondrial membrane potential (Rhodamine‐123), nuclei morphological change, and DNA fragmentation were examined by staining with DAPI. The results showed that both the BJ and BE venoms were capable of inhibiting tumor cell proliferation, promoting cytotoxicity and death by apoptosis of target SiHa and HeLa cells when treated with BJ and BE venoms. Furthermore, data revealed that both BJ venoms in SiHa cell promoted nuclear condensation, fragmentation, and formation of apoptotic bodies by DAPI assay, mitochondrial damage by Rhodamine‐123, and cell cycle block in the G1‐G0 phase. BJ and BE venoms present anticancer potential, suggesting that both Bothrops venoms could be used as prototypes for the development of new therapies.
Acute Marjolin’s Ulcer in a Postauricular Scar after Mastoidectomy
Authors: Alhysoni Kholoud A. , Bukhari Sumaiyah M. , Hajjaj Mutawakel F.
Published: December 2016

Background. Marjolin’s ulcer is a rare, aggressive cutaneous malignancy that arises primarily in burn scars but can occur in other types of scars. Squamous cell carcinoma is the most common variant, and while malignant degeneration usually takes a long time, it can develop acutely. Case Report. a 30-year-old man who developed Marjolin’s ulcer acutely in a right postauricular scar after mastoidectomy and the incision and drainage of a mastoid abscess. To the best of our knowledge, this report is the first to describe a Marjolin’s ulcer in a postauricular surgical scar. However, it has been reported in others areas in the head and neck. Conclusion. Marjolin’s ulcer is most commonly observed after postburn scars, but it may be observed after any type of scars, as our patient developed an SCC with a postsurgical scar. Early diagnosis is essential, and a biopsy should be performed on any nonhealing wound or chronic wound that undergoes a sudden change. Tissue samples should be taken from both the centre and the margins of the wound.
Analytical Modeling of a Ball Screw Feed Drive for Vibration Prediction of Feeding Carriage of a Spindle
Authors: Zhang Lei , Wang Taiyong , Tian Songling , Wang Yong
Published: December 2016

An analytical modeling approach for ball screw feed drives is proposed to predict the dynamic behavior of the feeding carriage of a spindle. Mainly considering the rigidity of linear guide modules, a ball-screw-feeding spindle is modeled by a mass-spring system. The contact stiffness of rolling interfaces in linear guide modules is accurately calculated according to the Hertzian theory. Next, a mathematical model is derived using the Lagrange method. The presented model is verified by conducting modal experiments. It is found that the simulated results correspond closely with the experimental data. In order to show the applicability of the proposed mathematical model, parameter-dependent dynamics of the feeding carriage of the spindle is investigated. The work will contribute to the vibration prediction of spindles.
Fusobacterium necrophorum Pharyngitis Complicated by Lemierre’s Syndrome
Authors: Faraone Antonio , Fortini Alberto , Nenci Gabriele , Boccadori Costanza , Mangani Valerio , Oggioni Roberto
Published: December 2016

We report the case of an 18-year-old woman who was referred to our outpatient clinic because of a 2-week history of sore throat, high fever, and neck tenderness unresponsive to a 7-day amoxicillin/clavulanic acid course. Infectious mononucleosis was initially suspected, but an extremely high value of procalcitonin and clinical deterioration suggested a bacterial sepsis, prompting the patient admission to our internal medicine ward. Blood cultures were positive for Fusobacterium necrophorum. CT scan detected a parapharyngeal abscess, a right internal jugular vein thrombosis, and multiple bilateral lung abscesses, suggesting the diagnosis of Lemierre’s syndrome. The patient was treated with a 2-week course of metronidazole and meropenem with a gradual clinical recovery. She was thereafter discharged home with metronidazole and amoxicillin/clavulanic acid for 14 days and a 3-month course of enoxaparin, experiencing an uneventful recovery. The present case highlights the importance of taking into consideration the Lemierre’s syndrome whenever a pharyngotonsillitis has a severe and unusual course.
An Ultra-Low Frequency Two DOFs’ Vibration Isolator Using Positive and Negative Stiffness in Parallel
Authors: Wang Min , Chen Xuedong , Li Xiaoqing
Published: December 2016

With the improvement of performance in the ultra-precision manufacturing engineering, the requirements for vibration isolation have become increasingly stringent. In order to get wider effective bandwidth and higher performance of vibration isolation in multiple DOFs system, an ultra-low frequency two DOFs’ vibration isolator with positive and negative stiffness in parallel (PNSP) is proposed. The two DOFs’ isolator which combines a positive stiffness (PS) air spring with a negative stiffness (NS) magnetic spring in parallel and combines a PS flat spring with an NS inverted pendulum in parallel is designed to reduce the natural frequency and broaden the effective bandwidth in horizontal and vertical direction. Based on this structure, stiffness models of different components in different directions are established. Compared with a PS isolator, it possesses the characteristic of high-static-low-dynamic stiffness. The simulation curves also provide strong evidence. Last, a real-time active control system and a spectrum testing and analysis system are used for the contrast experiment between the mentioned PNSP structure and PS only. The experimental results demonstrate that the isolator with PNSP can obviously reduce the natural frequency to 1 Hz and simultaneously maintain the stability of the system and consequently verify the validity and superiority of the mentioned structure.
Management of Giant Gastric Ulcer Perforation: Report of a Case and Review of the Literature
Authors: Vashistha Nitin , Singhal Dinesh , Makkar Gurpreet , Chakravarty Suneel , Raj Vivek
Published: December 2016

Giant gastric ulcer (GGU) is defined as an ulcer more than 3 cm in diameter. Now infrequent in clinical practice, in the pre-H2 receptor antagonist (H2RA) era, the incidence of GGU varied between 12 and 24% of all gastric ulcers. Proton pump inhibitors reportedly achieve better healing rates and symptom relief in comparison to H2RA. The GGU is associated with high incidence of serious complications such as hemorrhage. A perforated GGU though rare (<2%) offers serious challenges in management. We report one such case wherein the role of multidetector CT scan (MDCT) for diagnosis and treatment planning, surgical options for GGU perforations, and factors affecting outcome are discussed.
Fast and Robust Reconstruction for Fluorescence Molecular Tomography viaL1-2Regularization
Authors: Zhang Haibo , Geng Guohua , Wang Xiaodong , Qu Xuan , Hou Yuqing , He Xiaowei
Published: December 2016

Sparse reconstruction inspired by compressed sensing has attracted considerable attention in fluorescence molecular tomography (FMT). However, the columns of system matrix used for FMT reconstruction tend to be highly coherent, which meansL1minimization may not produce the sparsest solution. In this paper, we propose a novel reconstruction method by minimization of the difference ofL1andL2norms. To solve the nonconvexL1-2minimization problem, an iterative method based on the difference of convex algorithm (DCA) is presented. In each DCA iteration, the update of solution involves anL1minimization subproblem, which is solved by the alternating direction method of multipliers with an adaptive penalty. We investigated the performance of the proposed method with both simulated data andin vivoexperimental data. The results demonstrate that the DCA forL1-2minimization outperforms the representative algorithms forL1,L2,L1/2, andL0when the system matrix is highly coherent.
Understanding Lung Deposition of Alpha-1 Antitrypsin in Acute Experimental Mouse Lung Injury Model Using Fluorescence Microscopy
Authors: Wang Mengmeng , Zhan Yutian , Chen Jianqing , Rong Haojing , O’Neil Shawn P. , Ghosh Brahma , Nguyen Vuong , Owens Jane , Li Xianfeng , O’Hara Denise M.
Published: December 2016

Human plasma-derived α1-antitrypsin (AAT) delivered by intravenous infusion is used as augmentation therapy in patients with emphysema who have a genetic mutation resulting in deficiency of AAT. Inhalation is an alternative route of administration that can potentially increase the efficacy and convenience of treatment. This study was conducted to determine whether delivery to the lungs, initially via the intratracheal (IT) route of administration, would deliver efficacious levels of a recombinant AAT (rAAT) to the site of action in the lungs in mice. 125I-radiolabeled rAAT, fluorophore-conjugated rAAT (rAAT-Alexa488), and NE680 (neutrophil elastase 680, a silent fluorescent substrate of neutrophil elastase which fluoresces in the near-infrared range upon activation by neutrophil elastase) were used to characterize the pharmacokinetics and tissue distribution profile, distribution of rAAT within the lung, and efficacy of rAAT to inhibit neutrophil elastase at the site of action, respectively. The study has demonstrated that rAAT was able to gain access to locations where neutrophil elastase was localized. The histochemical quantification of rAAT activity relative to dose at the site of action provided here will improve confidence in predicting the human dose via the inhalation route.