bluuebunny/crossref_metadata_2025 huggingface dataset:
Cryptographically sound implementations for typed information-flow security
Authors: Fournet Cédric , Rezk Tamara
Published: August 2010

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues.

We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing.

We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We showtype soundness for a variant of the non-interference property, then show that our translation preserves typability.

We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.
Focusing and higher-order abstract syntax
Authors: Zeilberger Noam
Published: August 2010

Focusing is a proof-search strategy, originating in linear logic, that elegantly eliminates inessential nondeterminism, with one byproduct being a correspondence between focusing proofs and programs with explicit evaluation order. Higher-order abstract syntax (HOAS) is a technique for representing higher-order programming language constructs (e.g., λ's) by higher-order terms at the"meta-level", thereby avoiding some of the bureaucratic headaches of first-order representations (e.g., capture-avoiding substitution).

This paper begins with a fresh, judgmental analysis of focusing for intuitionistic logic (with a full suite of propositional connectives), recasting the "derived rules" of focusing as
iterated inductive definitions
. This leads to a uniform presentation, allowing concise, modular proofs of the identity and cut principles. Then we show how this formulation of focusing induces, through the Curry-Howard isomorphism, a new kind of higher-order encoding of abstract syntax: functions are encoded by maps from
patterns
to expressions. Dually, values are encoded as patterns together with
explicit substitutions
. This gives us pattern-matching "for free", and lets us reason about a rich type system with minimal syntactic overhead. We describe how to translate the language and proof of type safety almost directly into Coq using HOAS, and finally, show how the system's modular design pays off in enabling a very simple extension with recursion and recursive types.
An approach to call-by-name delimited continuations
Authors: Herbelin Hugo , Ghilezan Silvia
Published: August 2010

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λμ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λμ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus.
The design and implementation of typed scheme
Authors: Tobin-Hochstadt Sam , Felleisen Matthias
Published: August 2010

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants.

This paper presents Typed Scheme, an explicitly typed extension of an untyped scripting language. Its type system is based on the novel notion of
occurrence typing
, which we formalize and mechanically prove sound. The implementation of Typed Scheme additionally borrows elements from a range of approaches, including recursive types, true unions and subtyping, plus polymorphism combined with a modicum of local inference. Initial experiments with the implementation suggest that Typed Scheme naturally accommodates the programming style of the underlying scripting language, at least for the first few thousand lines of ported code.
Boomerang
Authors: Bohannon Aaron , Foster J. Nathan , Pierce Benjamin C. , Pilkiewicz Alexandre , Schmitt Alan
Published: August 2010

A
lens
is a bidirectional program. When read from left toright, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an ''update translator'' that takes an input together with an updated output and produces a new input that reflects the update. Many variants of this idea have been explored in the literature, but none deal fully with
ordered data
. If, for example, an update changes the order of a list in theoutput, the items in the output list and the chunks of the input that generated them can be misaligned, leading to lost or corrupted data.

We attack this problem in the context of bidirectional transformations over strings, the primordial ordered data type. We first propose a collection of bidirectional
string lens combinators
, based on familiar operations on regular transducers (union, concatenation, Kleene-star) and with a type system based on regular expressions. We then design anew semantic space of
dictionary lenses
, enriching the lenses of Foster et al. (2007) with support for two additional combinators for marking ''reorderable chunks'' andtheir keys. To demonstrate the effectiveness of these primitives, we describe the design and implementation of Boomerang, a full-blown
bidirectional programming language
with dictionary lenses at its core. We have used Boomerang to build transformers for complex real-world data format sincluding the SwissProt genomic database.

We formalize the essential property of
resourcefulness
-the correct use of keys to associate chunks in the input and output-by defining a refined semantic space of
quasi-oblivious lenses
. Several previously studied properties of lenses turn out to have compact characterizations in this space.
Resilient dictionaries
Authors: Finocchi Irene , Grandoni Fabrizio , Italiano Giuseppe F.
Published: August 2010

We address the problem of designing data structures in the presence of faults that may arbitrarily corrupt memory locations. More precisely, we assume that an adaptive adversary can arbitrarily overwrite the content of up to δ memory locations, that corrupted locations cannot be detected, and that only
O
(1) memory locations are safe. In this framework, we call a data structure resilient if it is able to operate correctly (at least) on the set of uncorrupted values. We present a resilient dictionary, implementing search, insert, and delete operations. Our dictionary has
O
(log
n
+ δ) expected amortized time per operation, and
O
(
n
) space complexity, where
n
denotes the current number of keys in the dictionary. We also describe a deterministic resilient dictionary, with the same amortized cost per operation over a sequence of at least δ
ϵ
operations, where ϵ > 0 is an arbitrary constant. Finally, we show that any resilient comparison-based dictionary must take Ω(log
n
+ δ) expected time per search. Our results are achieved by means of simple, new techniques which might be of independent interest for the design of other resilient algorithms.
An optimal decomposition algorithm for tree edit distance
Authors: Demaine Erik D. , Mozes Shay , Rossman Benjamin , Weimann Oren
Published: August 2010

The
edit distance
between two ordered rooted trees with vertex labels is the minimum cost of transforming one tree into the other by a sequence of elementary operations consisting of deleting and relabeling existing nodes, as well as inserting new nodes. In this article, we present a worst-case
O
(
n
3
)-time algorithm for the problem when the two trees have size
n
, improving the previous best
O
(
n
3
log
n
)-time algorithm. Our result requires a novel adaptive strategy for deciding how a dynamic program divides into subproblems, together with a deeper understanding of the previous algorithms for the problem. We prove the optimality of our algorithm among the family of
decomposition strategy
algorithms—which also includes the previous fastest algorithms—by tightening the known lower bound of Ω(
n
2
log
2
n
) to Ω(
n
3
), matching our algorithm's running time. Furthermore, we obtain matching upper and lower bounds for decomposition strategy algorithms of Θ(
nm
2
(1 + log
n
/
m
)) when the two trees have sizes
m
and
n
and
m
<
n
.
Approximating connectivity augmentation problems
Authors: Nutov Zeev
Published: August 2010

Let
G
= (
V
,
E
) be an undirected graph and let
S
⊆
V
. The
S-connectivity
λ

S

G

(
u
,
v
) of a node pair (
u
,
v
) in
G
is the maximum number of
uv
-paths that no two of them have an edge or a node in
S
- {
u
,
v
} in common. The corresponding Connectivity Augmentation (CA) problem is: given a graph
G
= (
V
,
E
), a node subset
S
⊆
V
, and a nonnegative integer requirement function
r
(
u
,
v
) on
V
×
V
, add a minimum size set
F
of new edges to
G
so that λ

S

G
+
F

(
u
,
v
) ≥
r
(
u
,
v
) for all (
u
,
v
) ∈
V
×
V
. Three extensively studied particular cases are: the Edge-CA (
S
= ∅), the Node-CA (
S
=
V
), and the Element-CA (
r
(
u
,
v
)= 0 whenever
u
∈
S
or
v
∈
S
). A polynomial-time algorithm for Edge-CA was developed by Frank. In this article we consider the Element-CA and the Node-CA, that are NP-hard even for
r
(
u
,
v
) ∈ {0,2}. The best known ratios for these problems were: 2 for Element-CA and
O
(
r
max
ṡ ln
n
) for Node-CA, where
r
max
= max

u

,

v

∈
V
r
(
u
,
v
) and
n
= |
V
|. Our main result is a 7/4-approximation algorithm for the Element-CA, improving the previously best known 2-approximation. For Element-CA with
r
(
u
,
v
) ∈ {0,1,2} we give a 3/2-approximation algorithm. These approximation ratios are based on a new splitting-off theorem, which implies an improved lower bound on the number of edges needed to cover a skew-supermodular set function. For Node-CA we establish the following approximation threshold: Node-CA with
r
(
u
,
v
) ∈ {0,
k
} cannot be approximated within
O
(2
log

1-ϵ
n

) for any fixed ϵ > 0, unless NP ⊆ DTIME(
n

polylog(
n
)

).
Low distortion spanners
Authors: Pettie Seth
Published: August 2010

A
spanner
of an undirected unweighted graph is a subgraph that approximates the distance metric of the original graph with some specified accuracy. Specifically, we say
H
⊆
G
is an
f
-spanner of
G
if any two vertices
u
,
v
at distance
d
in
G
are at distance at most
f
(
d
) in
H
. There is clearly some trade-off between the sparsity of
H
and the
distortion
function
f
, though the nature of the optimal trade-off is still poorly understood.

In this article we present a simple, modular framework for constructing sparse spanners that is based on interchangable components called
connection schemes
. By assembling connection schemes in different ways we can recreate the additive 2- and 6-spanners of Aingworth et al. [1999] and Baswana et al. [2009], and give spanners whose multiplicative distortion quickly tends toward 1. Our results rival the simplicity of all previous algorithms and provide substantial improvements (up to a doubly exponential reduction in edge density) over the comparable spanners of Elkin and Peleg [2004] and Thorup and Zwick [2006].
Latency-constrained aggregation in sensor networks
Authors: Becchetti LUCA , Marchetti-Spaccamela Alberto , Vitaletti Andrea , Korteweg Peter , Skutella Martin , Stougie Leen
Published: August 2010

A sensor network consists of sensing devices which may exchange data through wireless communication; sensor networks are highly energy constrained since they are usually battery operated. Data aggregation is a possible way to save energy consumption: nodes may delay data in order to aggregate them into a single packet before forwarding them towards some central node (sink). However, many applications impose constraints on the maximum delay of data; this translates into latency constraints for data arriving at the sink.

We study the problem of data aggregation to minimize maximum energy consumption under latency constraints on sensed data delivery, and we assume unique communication paths that form an intree rooted at the sink. We prove that the offline problem is strongly NP-hard and we design a 2-approximation algorithm. The latter uses a novel rounding technique.

Almost all real-life sensor networks are managed online by simple distributed algorithms in the nodes. In this context we consider both the case in which sensor nodes are synchronized or not. We assess the performance of the algorithm by competitive analysis. We also provide lower bounds for the models we consider, in some cases showing optimality of the algorithms we propose. Most of our results also hold when minimizing the total energy consumption of all nodes.
Improved online algorithms for the sorting buffer problem on line metrics
Authors: Gamzu Iftah , Segev Danny
Published: August 2010

An instance of the
sorting buffer
problem consists of a metric space and a server, equipped with a finite-capacity buffer capable of holding a limited number of requests. An additional ingredient of the input is an online sequence of requests, each of which is characterized by a destination in the given metric space; whenever a request arrives, it must be stored in the sorting buffer. At any point in time, a currently pending request can be served by drawing it out of the buffer and moving the server to its corresponding destination. The objective is to serve all input requests in a way that minimizes the total distance traveled by the server.

In this article, we focus our attention on instances of the problem in which the underlying metric is either an
evenly-spaced line metric
or a
continuous line metric
. Our main findings can be briefly summarized as follows.

(1) We present a
deterministic
O
(log
n
)-competitive algorithm for
n
-point evenly-spaced line metrics. This result improves on a randomized
O
(log
2
n
)-competitive algorithm due to Khandekar and Pandit [2006b]. It also refutes their conjecture, stating that a deterministic strategy is unlikely to obtain a nontrivial competitive ratio.

(2) We devise a
deterministic
O
(log
N
log log
N
)-competitive algorithm for continuous line metrics, where
N
denotes the length of the input sequence. In this context, we introduce a novel discretization technique of independent interest.

(3) We establish the first nontrivial lower bound for the evenly-spaced case, by proving that the competitive ratio of any deterministic algorithm is at least 2 + √3/√3 ≈ 2.154. This result settles, to some extent, an open question due to Khandekar and Pandit [2006b], who posed the task of attaining lower bounds on the achievable competitive ratio as a foundational objective for future research.
The Knuth-Yao quadrangle-inequality speedup is a consequence of total monotonicity
Authors: Bein Wolfgang , Golin Mordecai J. , Larmore Lawrence L. , Zhang Yan
Published: August 2010

There exist several general techniques in the literature for speeding up naive implementations of dynamic programming. Two of the best known are the Knuth-Yao quadrangle inequality speedup and the SMAWK algorithm for finding the row-minima of totally monotone matrices. Although both of these techniques use a quadrangle inequality and seem similar, they are actually quite different and have been used differently in the literature.

In this article we show that the Knuth-Yao technique is actually a direct consequence of total monotonicity. As well as providing new derivations of the Knuth-Yao result, this also permits to solve the Knuth-Yao problem directly using the SMAWK algorithm. Another consequence of this approach is a method for solving
online
versions of problems with the Knuth-Yao property. The online algorithms given here are asymptotically as fast as the best previously known static ones. For example, the Knuth-Yao technique speeds up the standard dynamic program for finding the optimal binary search tree of
n
elements from Θ(
n
3
) down to
O
(
n
2
), and the results in this article allow construction of an optimal binary search tree in an online fashion (adding a node to the left or the right of the current nodes at each step) in
O
(
n
) time per step.
Quantum algorithms for Simon's problem over nonabelian groups
Authors: Alagic Gorjan , Moore Cristopher , Russell Alexander
Published: August 2010

Daniel Simon's 1994 discovery of an efficient quantum algorithm for finding “hidden shifts” of Z
2

n

provided the first algebraic problem for which quantum computers are exponentially faster than their classical counterparts. In this article, we study the generalization of Simon's problem to arbitrary groups. Fixing a finite group
G
, this is the problem of recovering an involution
m
= (
m
1
,…,

m
n

) ∈

G
n

from an oracle
f
with the property that
f
(
x
⋅
y
) =
f
(
x
) ⇔
y
∈ {1,
m
}. In the current parlance, this is the hidden subgroup problem (HSP) over groups of the form

G
n

, where
G
is a nonabelian group of constant size, and where the hidden subgroup is either trivial or has order two.

Although groups of the form

G
n

have a simple product structure, they share important representation--theoretic properties with the symmetric groups

S
n

, where a solution to the HSP would yield a quantum algorithm for Graph Isomorphism. In particular, solving their HSP with the so-called “standard method” requires highly entangled measurements on the tensor product of many coset states.

In this article, we provide quantum algorithms with time complexity 2

O
(√
n
)

that recover hidden involutions
m
= (
m
1
,…

m
n

) ∈

G
n

where, as in Simon's problem, each

m
i

is either the identity or the conjugate of a known element
m
which satisfies κ(
m
) = −κ(1) for some κ ∈
Ĝ
. Our approach combines the general idea behind Kuperberg's sieve for dihedral groups with the “missing harmonic” approach of Moore and Russell. These are the first nontrivial HSP algorithms for group families that require highly entangled multiregister Fourier sampling.
Inverse auctions
Authors: Bruss F. Thomas , Louchard Guy , Ward Mark Daniel
Published: August 2010

We consider auctions in which the winning bid is the smallest bid that is unique. Only the upper-price limit is given. Neither the number of participants nor the distribution of the offers are known, so that the problem of placing a bid to win with maximum probability looks, a priori, ill-posed. Indeed, the essence of the problem is to inject a (final) minimum into a random subset (of unique offers) of a larger random set. We will see, however, that here no more than two external (and almost compelling) arguments make the problem meaningful. By appropriately modeling the relationship between the number of participants and the distribution of the bids, we can then maximize our chances of winning the auction and propose a computable algorithm for placing our bid.
A relational approach to interprocedural shape analysis
Authors: Jeannet Bertrand , Loginov Alexey , Reps Thomas , Sagiv Mooly
Published: August 2010

This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is,
interprocedural shape analysis
. The article makes three contributions.

— It introduces a new method for abstracting relations over memory configurations for use in abstract interpretation.

— It shows how this method furnishes the elements needed for a compositional approach to shape analysis. In particular, abstracted relations are used to represent the shape transformation performed by a sequence of operations, and an overapproximation to relational composition can be performed using the meet operation of the domain of abstracted relations.

— It applies these ideas in a new algorithm for context-sensitive interprocedural shape analysis. The algorithm creates procedure summaries using abstracted relations over memory configurations, and the meet-based composition operation provides a way to apply the summary transformer for a procedure
P
at each call site from which
P
is called.

The algorithm has been applied successfully to establish properties of both (i) recursive programs that manipulate lists and (ii) recursive programs that manipulate binary trees.
Hybrid type checking
Authors: Knowles Kenneth , Flanagan Cormac
Published: August 2010

Traditional static type systems are effective for verifying basic interface specifications. Dynamically checked contracts support more precise specifications, but these are not checked until runtime, resulting in incomplete detection of defects. Hybrid type checking is a synthesis of these two approaches that enforces precise interface specifications, via static analysis where possible, but also via dynamic checks where necessary. This article explores the key ideas and implications of hybrid type checking, in the context of the λ-calculus extended withcontract types, that is, with dependent function types and with arbitrary refinements of base types.
The complexity of temporal constraint satisfaction problems
Authors: Bodirsky Manuel , Kára Jan
Published: August 2010

A
temporal constraint language
is a set of relations that has a first-order definition in(Q;<), the dense linear order of the rational numbers. We present a complete complexity classification of the constraint satisfaction problem (CSP) for temporal constraint languages: if the constraint language is contained in one out of nine temporal constraint languages, then the CSP can be solved in polynomial time; otherwise, the CSP is NP-complete. Our proof combines model-theoretic concepts with techniques from universal algebra, and also applies the so-called product Ramsey theorem, which we believe will useful in similar contexts of constraint satisfaction complexity classification.

An extended abstract of this article appeared in the proceedings of STOC'08.
Privacy-preserving similarity-based text retrieval
Authors: Pang Hweehwa , Shen Jialie , Krishnan Ramayya
Published: August 2010

Users of online services are increasingly wary that their activities could disclose confidential information on their business or personal activities. It would be desirable for an online document service to perform text retrieval for users, while protecting the privacy of their activities. In this article, we introduce a privacy-preserving, similarity-based text retrieval scheme that (a) prevents the server from accurately reconstructing the term composition of queries and documents, and (b) anonymizes the search results from unauthorized observers. At the same time, our scheme preserves the relevance-ranking of the search server, and enables accounting of the number of documents that each user opens. The effectiveness of the scheme is verified empirically with two real text corpora.
Simulation modeling for analysis
Authors: Schruben Lee
Published: August 2010

This article explores possibilities for designing and executing simulation models with specific analysis goals in mind, and shows that a tight coupling of the modeling and analysis phases in a simulation project can lead to dramatic improvements in the study results. Suggestions are made for how simulation analysis, considered in the explicit context of discrete-event simulation models, can create new opportunities for meaningful research and more efficient modeling. Modeling decisions can play a significant role in the performance of analytical procedures. How a simulation model is designed can enable, inhibit, or even invalidate analytical procedures and methodology research results.
Simulation optimization using the cross-entropy method with optimal computing budget allocation
Authors: He Donghai , Lee Loo Hay , Chen Chun-Hung , Fu Michael C. , Wasserkrug Segev
Published: August 2010

We propose to improve the efficiency of simulation optimization by integrating the notion of optimal computing budget allocation into the Cross-Entropy (CE) method, which is a global optimization search approach that iteratively updates a parameterized distribution from which candidate solutions are generated. This article focuses on continuous optimization problems. In the stochastic simulation setting where replications are expensive but noise in the objective function estimate could mislead the search process, the allocation of simulation replications can make a significant difference in the performance of such global optimization search algorithms. A new allocation scheme is developed based on the notion of optimal computing budget allocation. The proposed approach improves the updating of the sampling distribution by carrying out this computing budget allocation in an efficient manner, by minimizing the expected mean-squared error of the CE weight function. Numerical experiments indicate that the computational efficiency of the CE method can be substantially improved if the ideas of computing budget allocation are applied.
Gradient estimation for discrete-event systems by measure-valued differentiation
Authors: Heidergott Bernd , Vázquez--Abad Felisa J. , Pflug Georg , Farenhorst-Yuan Taoying
Published: August 2010

In simulation of complex stochastic systems, such as Discrete-Event Systems (DES), statistical distributions are used to model the underlying randomness in the system. A sensitivity analysis of the simulation output with respect to parameters of the input distributions, such as the mean and the variance, is therefore of great value. The focus of this article is to provide a practical guide for robust sensitivity, respectively, gradient estimation that can be easily implemented along the simulation of a DES. We study the Measure-Valued Differentiation (MVD) approach to sensitivity estimation. Specifically, we will exploit the “modular” structure of the MVD approach, by firstly providing measure-valued derivatives for input distributions that are of importance in practice, and subsequently, by showing that if an input distribution possesses a measure-valued derivative, then so does the overall Markov kernel modeling the system transitions. This simplifies the complexity of applying MVD drastically: one only has to study the measure-valued derivative of the input distribution, a measure-valued derivative of the associated Markov kernel is then given through a simple formula in canonical form. The derivative representations of the underlying simple distributions derived in this article can be stored in a computer library. Combined with the generic MVD estimator, this yields an automated gradient estimation procedure. The challenge in automating MVD so that it can be included into a simulation package is the verification of the integrability condition to guarantee that the estimators are unbiased. The key contribution of the article is that we establish a general condition for unbiasedness which is easily checked in applications. Gradient estimators obtained by MVD are typically phantom estimators and we discuss the numerical efficiency of phantom estimators with the example of waiting times in the G/G/1 queue.
Young Massive Star Clusters
Authors: Portegies Zwart Simon F. , McMillan Stephen L.W. , Gieles Mark
Published: August 2010

Young massive clusters (YMCs) are dense aggregates of young stars that form the fundamental building blocks of galaxies. Several examples exist in the Milky Way Galaxy and the Local Group, but they are particularly abundant in starburst and interacting galaxies. The few YMCs that are close enough to resolve are of prime interest for studying the stellar mass function and the ecological interplay between stellar evolution and stellar dynamics. The distant unresolved clusters may be effectively used to study the star-cluster mass function, and they provide excellent constraints on the formation mechanisms of young cluster populations. YMCs are expected to be the nurseries for many unusual objects, including a wide range of exotic stars and binaries. So far only a few such objects have been found in YMCs, although their older cousins, the globular clusters, are unusually rich in stellar exotica. In this review, we focus on star clusters younger than ∼100 Myr, more than a few current crossing times old, and more massive than ∼104M⊙; the size of the cluster and its environment are considered less relevant as distinguishing parameters. We describe the global properties of the currently known young massive star clusters in the Local Group and beyond, and discuss the state of the art in observations and dynamical modeling of these systems. In order to make this review readable by observers, theorists, and computational astrophysicists, we also review the cross-disciplinary terminology.
Exoplanet Atmospheres
Authors: Seager Sara , Deming Drake
Published: August 2010

At the dawn of the first discovery of exoplanets orbiting Sun-like stars in the mid-1990s, few believed that observations of exoplanet atmospheres would ever be possible. After the 2002 Hubble Space Telescope detection of a transiting exoplanet atmosphere, many skeptics discounted it as a one-object, one-method success. Nevertheless, the field is now firmly established, with over two dozen exoplanet atmospheres observed today. Hot Jupiters are the type of exoplanet currently most amenable to study. Highlights include: detection of molecular spectral features, observation of day-night temperature gradients, and constraints on vertical atmospheric structure. Atmospheres of giant planets far from their host stars are also being studied with direct imaging. The ultimate exoplanet goal is to answer the enigmatic and ancient question, “Are we alone?” via detection of atmospheric biosignatures. Two exciting prospects are the immediate focus on transiting super Earths orbiting in the habitable zone of M-dwarfs, and ultimately the spaceborne direct imaging of true Earth analogs.
Interstellar Dust in the Solar System
Authors: Mann Ingrid
Published: August 2010

A fraction of the dust in the interstellar medium (ISM) enters the heliosphere and is measured in situ from spacecraft. This review surveys the in situ measurements and discusses a hence derived model of dust in the local interstellar cloud (LIC). The LIC dust model bears similarities to pristine cometary dust and is characteristic of the warm ISM clouds that fill a part of the ISM in the vicinity of the Sun. Recent and future dust in situ measurements provide a basis for closely studying physical processes in the ISM surrounding the Solar System. The LIC dust is the only dust component measurable in the Solar System that was not previously incorporated in larger Solar System objects. Issues for future LIC dust studies are measuring dust fluxes at the outer heliosphere, measuring the mass distribution with meteor observations and observations from spacecraft, and measuring the LIC dust composition in situ in space.
Searching for Insight
Authors: Lynden-Bell Donald
Published: August 2010

Is space-time only brought into being by its energy content? The jury is still out, but other questions that have been with me for much of my life—giant black holes in galactic nuclei, the formation of the Galaxy, the connection between first-order phase transitions and negative specific heats, the cause of the large-scale flow of galaxies relative to the cosmic microwave background—have all received reasonable answers. I have found great fun in understanding the dynamical mechanisms underlying such phenomena as magnetohydrodynamic jets, relativistic disks, and the bars, spirals, and chemical evolution of galaxies. The great challenges for future astronomers will be the exploration of the 96% of the Universe now believed to be neither atomic nor baryonic but perhaps partially leptonic. However, most advances do not come via frontal attack but from “bread-and-butter” investigations in related areas where observation is possible today!
Granular Cell Tumor of the Toe: A Case Report
Authors: Tamborini Federico , Cherubino Mario , Scamoni Stefano , Valdatta Luigi A.
Published: August 2010

Granular cell tumor is a rare tumor of unknown etiology that more commonly affects the oral cavity but can also occur at other sites. The majorities of granular cell tumors are benign and present as a singular dermal nodule. We discuss a case of granular cell tumor of the fourth toe in a 54‐year‐old patient that was treated with conservative surgery, instead of amputation, and reconstruction with a dermal regeneration template.
Disruption of Nrf2 Enhances the Upregulation of Nuclear Factor-kappaB Activity, Tumor Necrosis Factor-α, and Matrix Metalloproteinase-9 after Spinal Cord Injury in Mice
Authors: Mao Lei , Wang Handong , Qiao Liang , Wang Xiaoliang
Published: August 2010

Matrix metalloproteinase-9 (MMP-9) plays an important role in the acute periods of spinal cord injury (SCI), and its expression is related to the inflammation which could cause the disruption of the blood-spinal barrier (BBB). Nuclear factor erythroid 2-related factor 2 (Nrf2) is a key transcription factor that plays a crucial role in cytoprotection against inflammation. The present study investigated the role of Nrf2 in upregulating of nuclear factor kappa B (NF-κB) activity, tumor necrosis factor-α(TNF-α), and MMP-9 after SCI. Wild-type Nrf2 (+/+) and Nrf2-deficient (Nrf(−/−)) mice were subjected to an SCI model induced by the application of vascular clips (force of 10 g) to the dura after a three-level T8-T10 laminectomy. We detected the wet/dry weight ratio of impaired spinal cord tissue, the activation of NF-κB, the mRNA and protein levels of TNF-αand MMP-9, and the enzyme activity of MMP-9. Nrf2(−/−)mice were demonstrated to have more spinal cord edema, NF-κB activation, TNF-αproduction, and MMP-9 expression after SCI compared with the wild-type controls. The results suggest that Nrf2 may play an important role in limiting the upregulation of NF-κB activity, TNF-α, and MMP-9 in spinal cord after SCI.
Regional‐Scale Ozone Deposition to North‐East Atlantic Waters
Authors: Coleman L. , Varghese S. , Tripathi O. P. , Jennings S. G. , O′Dowd C. D.
Published: August 2010

A regional climate model is used to evaluate dry deposition of ozone over the North East Atlantic. Results are presented for a deposition scheme accounting for turbulent and chemical enhancement of oceanic ozone deposition and a second non‐chemical, parameterised gaseous dry deposition scheme. The first deposition scheme was constrained to account for sea‐surface ozone‐iodide reactions and the sensitivity of modelled ozone concentrations to oceanic iodide concentration was investigated. Simulations were also performed using nominal reaction rate derived from in-situ ozone deposition measurements and using a preliminary representation of organic chemistry. Results show insensitivity of ambient ozone concentrations modelled by the chemical‐enhanced scheme to oceanic iodide concentrations, and iodide reactions alone cannot account for observed deposition velocities. Consequently, we suggest a missing chemical sink due to reactions of ozone with organic matter at the air‐sea interface. Ozone loss rates are estimated to be in the range of 0.5–6 ppb per day. A potentially significant ozone‐driven flux of iodine to the atmosphere is estimated to be in the range of 2.5–500 M molec cm−2  s−1, leading to a mixing‐layer enhancement of organo‐iodine concentrations of 0.1–22.0 ppt, with an average increase in the N.E. Atlantic of around 4 ppt per day.
Dermoscopy of Cylindroma
Authors: Cabo Horacio , Pedrini Florencia , Cohen Sabban Emilia
Published: August 2010

Background. Dermoscopy provides additional criteria for the diagnosis of nonpigmented skin lesions. Case Report. An 80‐year‐old woman presented with an isolated, firm, dome‐shaped, erythematous nodule with surface telangiectasia on her forehead. Dermoscopy showed areas of background pink coloration with arborizing telangiectasia, blue dots/globules, and ulceration. Histologic analysis revealed features of cylindroma. Conclusion. Our case suggests that cylindromas may be added to the list of adnexal tumors mimicking BCC.
Impact of Congenital Heart Disease on Brain Development and Neurodevelopmental Outcome
Authors: Donofrio Mary T. , Massaro An N.
Published: August 2010

Advances in cardiac surgical techniques and perioperative intensive care have led to improved survival in babies with congenital heart disease (CHD). While it is true that the majority of children with CHD today will survive, many will have impaired neurodevelopmental outcome across a wide spectrum of domains. While continuing to improve short-term morbidity and mortality is an important goal, recent and ongoing research has focused on defining the impact of CHD on brain development, minimizing postnatal brain injury, and improving long-term outcomes. This paper will review the impact that CHD has on the developing brain of the fetus and infant. Neurologic abnormalities detectable prior to surgery will be described. Potential etiologies of these findings will be discussed, including altered fetal intrauterine growth, cerebral blood flow and brain development, associated congenital brain abnormalities, and risk for postnatal brain injury. Finally, reported neurodevelopmental outcomes after surgical repair of CHD will be reviewed.
Metallothionein-Like Proteins and Energy Reserve Levels after Ni and Pb Exposure in the Pacific White PrawnPenaeus vannamei
Authors: Nunez-Nogueira Gabriel , Mouneyrac Catherine , Muntz Alice , Fernandez-Bringas Laura
Published: August 2010

This study analyzed the changes in metallothionein-like proteins (MTLPs) and Energy Reserves (ERs) in hepatopancreas and abdominal muscle of the white prawnPenaeus vannamei. Realistic metal concentration exposure for 10 days to Ni and Pb in solution revealed that juvenile prawns partially induce MTLP in hepatopancreas after Pb exposure. Ni was distributed equally between soluble and insoluble fractions, while Pb was present only in the insoluble fraction, suggesting different detoxification strategy. No changes in lipids and glycogen concentration were detected under these experimental conditions in both tissues analyzed. MTLP could not be considered as a suitable indicator for lead exposure in hepatopancreas.
A Validated RP HPLC-PAD Method for the Determination of Hederacoside C in Ivy-Thyme Cough Syrup
Authors: Khdair Ayman , Mohammad Mohammad K. , Tawaha Khaled , Al-Hamarsheh Eman , AlKhatib Hatim S. , Al-khalidi Bashar , Bustanji Yasser , Najjar Samer , Hudaib Mohammad
Published: August 2010

A simple reversed phase high-performance liquid chromatographic (RP-HPLC) method coupled with a photodiode array detector (PAD) has been developed and validated for the analysis of hederacoside C, the marker of ivy plant, in Ivy-Thyme cough syrup. Separation of hederacoside C was achieved using a Phenomenex-Gemini C18 column isothermally at C. A mobile phase system constituted of solvent A (water: acetonitrile: orthophosphoric acid (85%), 860 : 140 : 2 v/v) and solvent B (acetonitrile: orthophosphoric acid (85%), 998 : 2 v/v) was used, at gradient conditions, at a flow rate of 1.5 mL/min. Analysis was performed using UV-detection (205 nm). The method was linear over the range (0.03–0.15) mg/mL of hederacoside C (). Repeatability and intermediate precision were acceptable (RSD %). Limits of detection (LOD) and quantitation (LOQ) were 0.011 and 0.032 mg/mL, respectively. Percentage recovery was found to lie between 99.69% and 100.90% (RSD %). The method was also proved to be specific (peak-purity ).
Giant Primary Retroperitoneal Teratoma in an Adult: A Case Report
Authors: Mathur Poonam , Lopez-Viego Miguel A. , Howell Myron
Published: August 2010

Teratomas are bizarre neoplasms derived from embryonic tissues that are typically found only in the gonadal and sacrococcygeal regions of adults. Retroperitoneal teratomas are rare and present challenging management options. We report here the case of a histologically unusual retroperitoneal tumor detected on computed tomography during the workup of abdominal pain in a 32-year-old male. The evaluation and treatment of this condition and a review of the literature are included in this paper.
A Solution of the Convective-Diffusion Equation for Solute Mass Transfer inside a Capillary Membrane Bioreactor
Authors: Godongwana B. , Solomons D. , Sheldon M. S.
Published: August 2010

This paper presents an analytical model of substrate mass transfer through the lumen of a membrane bioreactor. The model is a solution of the convective-diffusion equation in two dimensions using a regular perturbation technique. The analysis accounts for radial-convective flow as well as axial diffusion of the substrate specie. The model is applicable to the different modes of operation of membrane bioreactor (MBR) systems (e.g., dead-end, open-shell, or closed-shell mode), as well as the vertical or horizontal orientation. The first-order limit of the Michaelis-Menten equation for substrate consumption was used to test the developed model against available analytical results. The results obtained from the application of this model, along with a biofilm growth kinetic model, will be useful in the derivation of an efficiency expression for enzyme production in an MBR.
Laboratory Characterization and Influence of Mineralogy and Grading on the Performance of Treated and Untreated Granular Materials Used as Surface Pavements in Unpaved Road
Authors: Beaulieu L. , Pierre P. , Bilodeau J.-P.
Published: August 2010

This paper presents the results of a laboratory study on the influence of grading and granular mineralogy sources (granitic gneiss, basalt and limestone) on the performance of treated and untreated granular materials used as surface pavements in unpaved roads. Results of bearing capacity, resilient modulus and compressive strength tests are discussed. Natural brine, calcium chloride, cement and a polymer emulsion treated samples were tested and compared to untreated samples. The combinations of product, mineralogy and grading showing great performance are finally pointed out.
Novel Models of Myxoid Liposarcoma Xenografts Mimicking the Biological and Pharmacologic Features of Human Tumors
Authors: Frapolli Roberta , Tamborini Elena , Virdis Emanuela , Bello Ezia , Tarantino Eva , Marchini Sergio , Grosso Federica , Sanfilippo Roberta , Gronchi Alessandro , Tercero Juan Carlos , Peloso Gabriella , Casali Paolo , Pilotti Silvana , D'Incalci Maurizio
Published: August 2010

Purpose: Myxoid liposarcoma is a common subtype of liposarcoma. It is associated in more than 90% of cases with the chromosomal translocation t(12;16)(q13;p11) leading to the fusion FUS-CHOP gene that is responsible for the oncogenic transformation of preadipocytes. Recently the marine natural product trabectedin has shown highly selective activity for myxoid liposarcoma, even in the most aggressive round-cell subtype.

Experimental Design: Fragments of 17 sarcomas were transplanted s.c. in female athymic NCr-nu/nu mice. Xenografts were established and characterized by morphology, fluorescence in situ hybridization analysis for the translocation and reverse transcriptase-PCR analysis for fusion transcripts. Trabectedin was injected i.v.

Results: Seven of 17 tumors grew as continuous xenografts, five of them being myxoid liposarcoma of the round-cell subtype. The chromosomal rearrangement and fusion transcripts in different passages were the same as in the human tumors from which they were derived. The responsiveness to trabectedin in type II myxoid liposarcoma xenografts was as high as in patients. The pathologic response was associated with the presence of the FUS-CHOP fusion gene, indicating that the drug does not totally eradicate the disease. Type III myxoid liposarcoma xenografts seemed much less sensitive to trabectedin, confirming previous clinical observations.

Conclusions: This study reports for the first time the characterization of human myxoid liposarcoma xenografts that adequately mimic the biological and pharmacologic features of the human tumor. These models offer a useful tool for investigating the mechanism of selectivity of trabectedin, testing new combinations with this drug and evaluating novel therapies for myxoid liposarcoma. Clin Cancer Res; 16(20); 4958–67. ©2010 AACR.
Dynamic MicroRNA Expression Programs During Cardiac Differentiation of Human Embryonic Stem Cells
Authors: Wilson Kitchener D. , Hu Shijun , Venkatasubrahmanyam Shivkumar , Fu Ji-Dong , Sun Ning , Abilez Oscar J. , Baugh Joshua J.A. , Jia Fangjun , Ghosh Zhumur , Li Ronald A. , Butte Atul J. , Wu Joseph C.
Published: August 2010

Background—

MicroRNAs (miRNAs) are a newly discovered endogenous class of small, noncoding RNAs that play important posttranscriptional regulatory roles by targeting messenger RNAs for cleavage or translational repression. Human embryonic stem cells are known to express miRNAs that are often undetectable in adult organs, and a growing body of evidence has implicated miRNAs as important arbiters of heart development and disease.

Methods and Results—

To better understand the transition between the human embryonic and cardiac “miRNA-omes,” we report here the first miRNA profiling study of cardiomyocytes derived from human embryonic stem cells. Analyzing 711 unique miRNAs, we have identified several interesting miRNAs, including miR-1, -133, and -208, that have been previously reported to be involved in cardiac development and disease and that show surprising patterns of expression across our samples. We also identified novel miRNAs, such as miR-499, that are strongly associated with cardiac differentiation and that share many predicted targets with miR-208. Overexpression of miR-499 and -1 resulted in upregulation of important cardiac myosin heavy-chain genes in embryoid bodies; miR-499 overexpression also caused upregulation of the cardiac transcription factor MEF2C.

Conclusions—

Taken together, our data give significant insight into the regulatory networks that govern human embryonic stem cell differentiation and highlight the ability of miRNAs to perturb, and even control, the genes that are involved in cardiac specification of human embryonic stem cells.