bluuebunny/crossref_metadata_2025 huggingface dataset:
Great Lakes Environmental Protection Policies from a Fisheries Perspective
Authors: Johnson M. G.
Published: January 2010

International policies in environmental protection and resources management in the Great Lakes have evolved in three fields: water quantity and quality management, fisheries management, and air pollution abatement. The general segregation of policy development ignores the complex interplay among air, water, and fisheries resources and the potential to direct wastes to selected receptors. Approaches to environmental and resources management do not deal effectively with root causes in a sufficiently broad context. Socioeconomic information is not used effectively either as yardsticks of environmental quality or as compelling arguments for remedial programs. New approaches are needed toward resources management cum environmental policy, with emphasis on participatory planning across resource sectors to optimize a diversity of long-term benefits to society. Strong political leadership is required to depolarize jurisdictional and bureaucratic empires. The International Joint Commission and Great Lakes Fishery Commission should collaborate to help in identification of issues and root causes, to encourage strategic planning with resource sector and public participation, and to take a broad overview of societal goals and public policy in relation to recognized finite capacity of the Great Lakes ecosystem to maintain quality of life as a long-term premise.Key words: ecosystems, resource management, fisheries management, environmental legislation, international cooperation, international agreements, sociological aspects
FORMATION OF A NOVEL HARD BINARY SiO2/QUANTUM DOT NANOCOMPOSITE WITH PREDICTABLE ELECTRICAL CONDUCTIVITY
Authors: ALIOV M. K. , SABUR A. R.
Published: January 2010

In this paper, hard silica/epoxy nanocomposite coatings were prepared by a spinning method on the surface of AA6082 aluminum alloy with addition of CdTe quantum dots as the second phase in hard nanocomposite coating with different ratios with respect to main phase (silica nanoparticulates). Wear and electrical conductivity test have been done on the coatings for investigation of the possible enhanced or inverse effects of addition QDs on properties of hard nanocomposite. The effect of coating time, rotating speed and SiO 2/QD ratio have been investigated and it has been shown that by adding QD nanoparticulates, the electrical conductivity of layers is completely controllable without adverse effect on wear resistance. The effects of mentioned parameters on the trend of obtained curves have been discussed.
ON THE HIGH ACCURACY NS-ALPHA-DECONVOLUTION TURBULENCE MODEL
Authors: REBHOLZ LEO G. , SUSSMAN MYRON M.
Published: January 2010

We analyze the mathematical and physical properties of, and present numerical experiments for, the recently proposed NS-α-deconvolution model of fluid turbulence. This family of models has the well-known NS-α model as its zeroth-order model, and applies the Nth van Cittert deconvolution operator to the filtered terms in NS-α to create the Nth-order NS-α-deconvolution model. This model is proposed in Ref. 29, where it is shown to have consistency error O(α2N + 2). Herein we prove that the model admits unique regular solutions, is frame invariant, and improves the consistency error of NS-α from O(α2) to O(α2N + 2) while requiring (N + 1)1/2 times more (typically 1 ≤ N ≤ 5) degrees of freedom for complete resolution. Numerical experiments show that adding approximate deconvolution to NS-α significantly improves accuracy in computations.
Undecidability and intractability results concerning datalog programs and their persistency numbers
Authors: Cosmadakis Stavros , Foustoucos Eugenie , Sidiropoulos Anastasios
Published: January 2010

The relation between Datalog programs and homomorphism problems, and, between Datalog programs and bounded treewidth structures has been recognized for some time and given much attention recently. Additionally, the essential role of persistent variables (in program expansions) for solving several relevant problems has also started to be observed. In Afrati et al. [2005] the general notion of program persistencies was refined into four notions (two syntactical ones and two semantical ones) and the interrelationship between these four
persistency numbers
was studied. In the present article (1) we prove undecidability results concerning the semantical notions of persistency number--modulo equivalence, of persistency number and of characteristic integer, (2) we exhibit new classes of programs for which boundedness is undecidable and (3) we prove intractabiltity results concerning the syntactical notions of weak persistency number and of weak characteristic integer.
On the verification problem for weak memory models
Authors: Atig Mohamed Faouzi , Bouajjani Ahmed , Burckhardt Sebastian , Musuvathi Madanlal
Published: January 2010

We address the verification problem of finite-state concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multi-processor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performance-critical system services employing lock-free synchronization, as well as for the correctness of compiler backends that generate code targeted to run on such architectures.

We consider in this paper combinations of three well-known program order relaxations. We consider first the "write to read" relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the "write to write" relaxation, leading to a model which is essentially PSO (Partial Store Ordering), or (2) the "read to read/write" relaxation, or (3) both of them, as it is done in the RMO (Relaxed Memory Ordering) model for instance.

We define abstract operational models for these weak memory models based on state machines with (potentially unbounded) FIFO buffers, and we investigate the decidability of their reachability and their repeated reachability problems.

We prove that the reachability problem is decidable for the TSO model, as well as for its extension with "write to write" relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the "read to read/write" relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. We show also that the repeated reachability problem is undecidable for all the considered memory models.
Sequential verification of serializability
Authors: Attiya H. , Ramalingam G. , Rinetzky N.
Published: January 2010

Serializability is a commonly used correctness condition in concurrent programming. When a concurrent module is serializable, certain other properties of the module can be verified by considering only its sequential executions. In many cases, concurrent modules guarantee serializability by using standard locking protocols, such as tree locking or two-phase locking. Unfortunately, according to the existing literature, verifying that a concurrent module adheres to these protocols requires considering concurrent interleavings.

In this paper, we show that adherence to a large class of locking protocols (including tree locking and two-phase locking) can be verified by considering only
sequential
executions. The main consequence of our results is that in many cases, the (manual or automatic)
verification of serializability can itself be done using sequential reasoning
.
Continuity analysis of programs
Authors: Chaudhuri Swarat , Gulwani Sumit , Lublinerman Roberto
Published: January 2010

We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the
robustness
of programs whose inputs can have small amounts of error and uncertainty---e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.

Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate ``synchronization points'' between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.
A verified compiler for an impure functional language
Authors: Chlipala Adam
Published: January 2010

We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq's tactic language, making it possible to reuse proofs unchanged as new language features are added.

In this paper, we focus especially on phases of compilation that rearrange the structure of syntax with nested variable binders. That aspect has been a key challenge area in past compiler verification projects, with much more effort expended in the statement and proof of binder-related lemmas than is found in standard pencil-and-paper proofs. We show how to exploit the representation technique of parametric higher-order abstract syntax to avoid the need to prove any of the usual lemmas about binder manipulation, often leading to proofs that are actually shorter than their pencil-and-paper analogues. Our strategy is based on a new approach to encoding operational semantics which delegates all concerns about substitution to the meta language, without using features incompatible with general-purpose type theories like Coq's logic.
Dependent types from counterexamples
Authors: Terauchi Tachio
Published: January 2010

Motivated by recent research in abstract model checking, we present a new approach to inferring dependent types. Unlike many of the existing approaches, our approach does not rely on programmers to supply the candidate (or the correct) types for the recursive functions and instead does counterexample-guided refinement to automatically generate the set of candidate dependent types. The main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found untypable with the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real type error or generate additional candidate dependent types to refute the spurious counterexample. The process is repeated until either a real type error is found or sufficient candidates are generated to prove the program typable. Our system makes non-trivial use of "linear" intersection types in the refinement phase.

The paper presents the type inference system and reports on the experience with a prototype implementation that infers dependent types for a subset of the Ocaml language. The implementation infers dependent types containing predicates from the quantifier-free theory of linear arithmetic and equality with uninterpreted function symbols.
Low-level liquid types
Authors: Rondon Patrick Maxim , Kawaguchi Ming , Jhala Ranjit
Published: January 2010

We present
Low-Level Liquid Types
, a refinement type system for C based on
Liquid Types
. Low-Level Liquid Types combine refinement types with three key elements to automate verification of critical safety properties of low-level programs: First, by associating refinement types with individual heap locations and precisely tracking the locations referenced by pointers, our system is able to reason about complex invariants of in-memory data structures and sophisticated uses of pointer arithmetic. Second, by adding constructs which allow strong updates to the types of heap locations, even in the presence of aliasing, our system is able to verify properties of in-memory data structures in spite of temporary invariant violations. By using this strong update mechanism, our system is able to verify the correct initialization of newly-allocated regions of memory. Third, by using the abstract interpretation framework of Liquid Types, we are able to use refinement type inference to automatically verify important safety properties without imposing an onerous annotation burden. We have implemented our approach in CSOLVE, a tool for Low-Level Liquid Type inference for C programs. We demonstrate through several examples that CSOLVE is able to precisely infer complex invariants required to verify important safety properties, like the absence of array bounds violations and null-dereferences, with a minimal annotation overhead.
Type inference for datalog with complex type hierarchies
Authors: Schäfer Max , de Moor Oege
Published: January 2010

Type inference for Datalog can be understood as the problem of mapping programs to a sublanguage for which containment is decidable. To wit, given a program in Datalog, a schema describing the types of extensional relations, and a user-supplied set of facts about the basic types (stating conditions such as disjointness, implication or equivalence), we aim to infer an over-approximation of the semantics of the program, which should be expressible in a suitable sublanguage of Datalog.

We argue that Datalog with monadic extensionals is an appropriate choice for that sublanguage of types, and we present an inference algorithm. The inference algorithm is proved sound, and we also show that it infers the tightest possible over-approximation for a large class of Datalog programs. Furthermore, we present a practical containment check for a large subset of our type language. The crux of that containment check is a novel generalisation of Quine's procedure for computing prime implicants. The type system has been implemented in a state-of-the-art industrial database system, and we report on experiments with this implementation.
Nominal system T
Authors: Pitts Andrew M.
Published: January 2010

This paper introduces a new recursion principle for inductive data modulo α-equivalence of bound names. It makes use of Odersky-style local names when recursing over bound names. It is formulated in an extension of Gödel's System T with names that can be tested for equality, explicitly swapped in expressions and restricted to a lexical scope. The new recursion principle is motivated by the nominal sets notion of "α-structural recursion", whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. The new
Nominal System T
presented here provides a calculus of total functions that is shown to adequately represent α-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. Adequacy is proved via a normalization-by-evaluation argument that makes use of a new semantics of local names in Gabbay-Pitts nominal sets.
A theory of indirection via approximation
Authors: Hobor Aquinas , Dockins Robert , Appel Andrew W.
Published: January 2010

Building semantic models that account for various kinds of indirect reference has traditionally been a difficult problem. Indirect reference can appear in many guises, such as heap pointers, higher-order functions, object references, and shared-memory mutexes.

We give a general method to construct models containing indirect reference by presenting a "theory of indirection". Our method can be applied in a wide variety of settings and uses only simple, elementary mathematics. In addition to various forms of indirect reference, the resulting models support powerful features such as impredicative quantification and equirecursion; moreover they are compatible with the kind of powerful substructural accounting required to model (higher-order) separation logic. In contrast to previous work, our model is easy to apply to new settings and has a simple axiomatization, which is complete in the sense that all models of it are isomorphic. Our proofs are machine-checked in Coq.
A relational modal logic for higher-order stateful ADTs
Authors: Dreyer Derek , Neis Georg , Rossberg Andreas , Birkedal Lars
Published: January 2010

The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, strongly normalizing languages like System F, it has been extended over the past two decades to reason about increasingly realistic languages. In particular, Appel and McAllester's idea of step-indexing has been used recently to develop syntactic Kripke logical relations for ML-like languages that mix functional and imperative forms of data abstraction. However, while step-indexed models are powerful tools, reasoning with them directly is quite painful, as one is forced to engage in tedious step-index arithmetic to derive even simple results.

In this paper, we propose a logic LADR for equational reasoning about higher-order programs in the presence of existential type abstraction, general recursive types, and higher-order mutable state. LADR exhibits a novel synthesis of features from Plotkin-Abadi logic, Gödel-Löb logic, S4 modal logic, and relational separation logic. Our model of LADR is based on Ahmed, Dreyer, and Rossberg's state-of-the-art step-indexed Kripke logical relation, which was designed to facilitate proofs of representation independence for "state-dependent" ADTs. LADR enables one to express such proofs at a much higher level, without counting steps or reasoning about the subtle, step-stratified construction of possible worlds.
Counterexample-guided focus
Authors: Podelski Andreas , Wies Thomas
Published: January 2010

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right treatment of disjunction below and above the universal quantifier. In the closely related setting of shape analysis one uses the focus operator in order to adapt the treatment of disjunction (and thus the efficiency-precision tradeoff) to the individual program statement. One promising research direction is to design parameterized versions of the focus operator which allow the user to fine-tune the focus operator not only to the individual program statements but also to the specific verification task. We carry this research direction one step further. We fine-tune the focus operator to each individual step of the analysis (for a specific verification task). This fine-tuning must be done automatically. Our idea is to use counterexamples for this purpose. We realize this idea in a tool that automatically infers quantified invariants for the verification of a variety of heap-manipulating programs.
Dependent types and program equivalence
Authors: Jia Limin , Zhao Jianzhou , Sjöberg Vilhelm , Weirich Stephanie
Published: January 2010

The definition of type equivalence is one of the most important design issues for any typed language. In dependently typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation.

Almost all dependently-typed languages require this relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML, ATS, Ωmega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. Instead, they identify a terminating index language and use singleton types to connect indices to computation. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness.

Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify total correctness properties. However, decidable type checking is not a prerequisite for type safety. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may not be useful in practice.

Therefore, we take a different approach: instead of a fixed notion for term equivalence, we parameterize our type system with an abstract relation that is not necessarily decidable. We then design a novel set of typing rules that require only weak properties of this abstract relation in the proof of the preservation and progress lemmas. This design provides flexibility: we compare valid instantiations of term equivalence which range from beta-equivalence, to contextual equivalence, to some exotic equivalences.
Modular session types for distributed object-oriented programming
Authors: Gay Simon J. , Vasconcelos Vasco T. , Ravara António , Gesbert Nils , Caldeira Alexandre Z.
Published: January 2010

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be
modularized
, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. We also describe a prototype implementation as an extension of Java.
Generating compiler optimizations from proofs
Authors: Tate Ross , Stepp Michael , Lerner Sorin
Published: January 2010

We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.

We present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging type errors.

Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations from expensive-to-run super-optimizers.
Automatically generating instruction selectors using declarative machine descriptions
Authors: Dias João , Ramsey Norman
Published: January 2010

Despite years of work on retargetable compilers, creating a good, reliable back end for an optimizing compiler still entails a lot of hard work. Moreover, a critical component of the back end---the instruction selector---must be written by a person who is expert in both the compiler's intermediate code and the target machine's instruction set. By
generating
the instruction selector from declarative machine descriptions we have (a) made it unnecessary for one person to be both a compiler expert and a machine expert, and (b) made creating an optimizing back end easier than ever before.

Our achievement rests on two new results. First, finding a mapping from intermediate code to machine code is an undecidable problem. Second, using heuristic search, we can find mappings for machines of practical interest in at most a few minutes of CPU time.

Our most significant new idea is that heuristic search should be controlled by algebraic laws. Laws are used not only to show when a sequence of instructions implements part of an intermediate code, but also to limit the search: we drop a sequence of instructions not when it gets too long or when it computes too complicated a result, but when
too much reasoning
will be required to show that the result computed might be useful.
Semantics and algorithms for data-dependent grammars
Authors: Jim Trevor , Mandelbaum Yitzhak , Walker David
Published: January 2010

We present the design and theory of a new parsing engine, YAKKER, capable of satisfying the many needs of modern programmers and modern data processing applications. In particular, our new parsing engine handles (1) full scannerless context-free grammars with (2) regular expressions as right-hand sides for defining nonterminals. YAKKER also includes (3) facilities for binding variables to intermediate parse results and (4) using such bindings within arbitrary constraints to control parsing. These facilities allow the kind of data-dependent parsing commonly needed in systems applications, particularly those that operate over binary data. In addition, (5) nonterminals may be parameterized by arbitrary values, which gives the system good modularity and abstraction properties in the presence of data-dependent parsing. Finally, (6) legacy parsing libraries,such as sophisticated libraries for dates and times, may be directly incorporated into parser specifications. We illustrate the importance and utility of this rich collection of features by presenting its use on examples ranging from difficult programming language grammars to web server logs to binary data specification. We also show that our grammars have important compositionality properties and explain why such properties areimportant in modern applications such as automatic grammar induction.

In terms of technical contributions, we provide a traditional high-level semantics for our new grammar formalization and show how to compile grammars into non deterministic automata. These automata are stack-based, somewhat like conventional push-down automata,but are also equipped with environments to track data-dependent parsing state. We prove the correctness of our translation of data-dependent grammars into these new automata and then show how to implement the automata efficiently using a variation of Earley's parsing algorithm.
Modular verification of security protocol code by typing
Authors: Bhargavan Karthikeyan , Fournet Cédric , Gordon Andrew D.
Published: January 2010

We propose a method for verifying the security of protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. We develop cryptographic libraries that embed a logic model of their cryptographic structures and that specify preconditions and postconditions on their functions so as to maintain their invariants. We present a theory to justify the soundness of modular code verification via our method.

We implement the method for protocols coded in F# and verified using F7, our SMT-based typechecker for refinement types, that is, types carrying formulas to record invariants. As illustrated by a series of programming examples, our method can flexibly deal with a range of different cryptographic constructions and protocols.

We evaluate the method on a series of larger case studies of protocol code, previously checked using whole-program analyses based on ProVerif, a leading verifier for cryptographic protocols. Our results indicate that compositional verification by typechecking with refinement types is more scalable than the best domain-specific analysis currently available for cryptographic code.
Dynamically checking ownership policies in concurrent c/c++ programs
Authors: Martin Jean-Phillipe , Hicks Michael , Costa Manuel , Akritidis Periklis , Castro Miguel
Published: January 2010

Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either
owned exclusively
by a thread that can read or write the data, or it is
read owned
by a set of threads that can read but not write the data. Unfortunately, incorrect synchronization often fails to enforce these policies and memory errors in languages like C and C++ can violate these policies even when synchronization is correct.

In this paper, we present a dynamic analysis for checking ownership policies in concurrent C and C++ programs despite memory errors. The analysis can be used to find errors in commodity multi-threaded programs and to prevent attacks that exploit these errors. We require programmers to write ownership assertions that describe the sharing policies used by different parts of the program. These policies may change over time, as may the policies' means of enforcement, whether it be locks, barriers, thread joins, etc. Our compiler inserts checks in the program that signal an error if these policies are violated at runtime. We evaluated our tool on several benchmark programs. The run-time overhead was reasonable: between 0 and 49% with an average of 26%. We also found the tool easy to use: the total number of ownership assertions is small, and the asserted specification and implementation can be debugged together by running the instrumented program and addressing the errors that arise. Our approach enjoys a pleasing modular soundness property: if a thread executes a sequence of statements on variables it owns, the statements are serializable within a valid execution, and thus their effects can be reasoned about in isolation from other threads in the program.
Regulation of the Actin Cytoskeleton-Plasma Membrane Interplay by Phosphoinositides
Authors: Saarikangas Juha , Zhao Hongxia , Lappalainen Pekka
Published: January 2010

The plasma membrane and the underlying cortical actin cytoskeleton undergo continuous dynamic interplay that is responsible for many essential aspects of cell physiology. Polymerization of actin filaments against cellular membranes provides the force for a number of cellular processes such as migration, morphogenesis, and endocytosis. Plasma membrane phosphoinositides (especially phosphatidylinositol bis- and trisphosphates) play a central role in regulating the organization and dynamics of the actin cytoskeleton by acting as platforms for protein recruitment, by triggering signaling cascades, and by directly regulating the activities of actin-binding proteins. Furthermore, a number of actin-associated proteins, such as BAR domain proteins, are capable of directly deforming phosphoinositide-rich membranes to induce plasma membrane protrusions or invaginations. Recent studies have also provided evidence that the actin cytoskeleton-plasma membrane interactions are misregulated in a number of pathological conditions such as cancer and during pathogen invasion. Here, we summarize the wealth of knowledge on how the cortical actin cytoskeleton is regulated by phosphoinositides during various cell biological processes. We also discuss the mechanisms by which interplay between actin dynamics and certain membrane deforming proteins regulate the morphology of the plasma membrane.
Pathophysiology of Sleep Apnea
Authors: Dempsey Jerome A. , Veasey Sigrid C. , Morgan Barbara J. , O'Donnell Christopher P.
Published: January 2010

Sleep-induced apnea and disordered breathing refers to intermittent, cyclical cessations or reductions of airflow, with or without obstructions of the upper airway (OSA). In the presence of an anatomically compromised, collapsible airway, the sleep-induced loss of compensatory tonic input to the upper airway dilator muscle motor neurons leads to collapse of the pharyngeal airway. In turn, the ability of the sleeping subject to compensate for this airway obstruction will determine the degree of cycling of these events. Several of the classic neurotransmitters and a growing list of neuromodulators have now been identified that contribute to neurochemical regulation of pharyngeal motor neuron activity and airway patency. Limited progress has been made in developing pharmacotherapies with acceptable specificity for the treatment of sleep-induced airway obstruction. We review three types of major long-term sequelae to severe OSA that have been assessed in humans through use of continuous positive airway pressure (CPAP) treatment and in animal models via long-term intermittent hypoxemia (IH): 1) cardiovascular. The evidence is strongest to support daytime systemic hypertension as a consequence of severe OSA, with less conclusive effects on pulmonary hypertension, stroke, coronary artery disease, and cardiac arrhythmias. The underlying mechanisms mediating hypertension include enhanced chemoreceptor sensitivity causing excessive daytime sympathetic vasoconstrictor activity, combined with overproduction of superoxide ion and inflammatory effects on resistance vessels. 2) Insulin sensitivity and homeostasis of glucose regulation are negatively impacted by both intermittent hypoxemia and sleep disruption, but whether these influences of OSA are sufficient, independent of obesity, to contribute significantly to the “metabolic syndrome” remains unsettled. 3) Neurocognitive effects include daytime sleepiness and impaired memory and concentration. These effects reflect hypoxic-induced “neural injury.” We discuss future research into understanding the pathophysiology of sleep apnea as a basis for uncovering newer forms of treatment of both the ventilatory disorder and its multiple sequelae.
Low‐Frequency Low‐Intensity Ultrasounds Do Not Influence the Survival and Immune Functions of Cultured Keratinocytes and Dendritic Cells
Authors: Scarponi Claudia , Nasorri Francesca , Pavani Francesca , Madonna Stefania , Sestito Rosanna , Simonacci Marco , De Pità Ornella , Cavani Andrea , Albanesi Cristina
Published: January 2010

Low‐frequency ultrasounds (US) are used to enhance drug transdermal transport. Although this phenomenon has been extensively analyzed, information on US effects on the single skin cell components is limited. Here, we investigated the possible effects of low‐frequency US on viability and immune functions of cultured human keratinocytes and dendritic cells (DC), skin cells involved in the regulation of many immune‐mediated dermatoses. We demonstrated that US, employed at low‐frequency (42 KHz) and low‐intensity (0.15 W/cm2) values known to enhance drug and water transdermal transport, did not affect extracellular‐signal‐regulated‐kinase (ERK)1/2 activation, cell viability, or expression of adhesion molecules in cultured keratinocytes. Moreover, US at these work frequency and intensity did not influence the keratinocyte expression and release of immunomodulatory molecules. Similarly, cultured DC treated with low‐frequency low‐intensity US were viable, and did not show an altered membrane phenotype, cytokine profile, nor antigen presentation ability. However, intensity enhancement of low‐frequency US to 5 W/cm2 determined an increase of the apoptotic rate of both keratinocytes and DC as well as keratinocyte CXCL8 release and ERK1/2 activation, and DC CD40 expression. Our study sustains the employment of low‐frequency and low‐intensity US for treatment of those immune skin disorders, where keratinocytes and DC have a pathogenetic role.
Collaborative Assembly Operation between Two Modular Robots Based on the Optical Position Feedback
Authors: Su Liying , Shi Lei , Yu Yueqing
Published: January 2010

This paper studies the cooperation between two master-slave modular robots. A cooperative robot system is set up with two modular robots and a dynamic optical meter-Optotrak. With Optotrak, the positions of the end effectors are measured as the optical position feedback, which is used to adjust the robots' end positions. A tri-layered motion controller is designed for the two cooperative robots. The RMRC control method is adopted to adjust the master robot to the desired position. With the kinematics constraints of the two robots including position and pose, joint velocity, and acceleration constraints, the two robots can cooperate well. A bolt and nut assembly experiment is executed to verify the methods.
Effect and Risk of AEE788, a Dual Tyrosine Kinase Inhibitor, on Regeneration in a Rat Liver Resection Model
Authors: Deng M. , Huang H. , Dirsch O. , Dahmen U.
Published: January 2010

Background: AEE788, a dual tyrosine kinase inhibitor, has antiproliferative effects on diverse tumor models in mice. We aimed to investigate whether AEE788 blocks liver regeneration and causes drug-related side effects. Methods: Rats treated orally with 50 mg/kg AEE788 or solvent every 2 days were subjected to 70% partial hepatectomy (PH) and sacrificed on postoperative days 1, 2, 7, and 28. Liver regeneration was evaluated using liver weight to body weight ratio, BrdU-staining, mitotic index, and PCR for PCNA (proliferating cell nuclear antigen). Side effects on the gastrointestinal system and liver were assessed using clinical chemistry, histology, silver staining, and immunohistochemistry. Plasma and liver tissue levels of AEE788 were measured using spectrometry. Results: AEE788 treatment did not inhibit liver regeneration. No obvious drug-related systemic or hepatic side effects were observed. Restoration of liver architecture during liver regeneration was not obviously impaired, even after 4 weeks’ AEE788 treatment. After a 1-week treatment, AEE788 concentrations in plasma and liver tissue in the PH group were 3-fold and 8-fold higher than the non-PH group, respectively. Conclusion: Its antiproliferative properties, good tolerance, and lack of inhibition on liver regeneration make AEE788 a potential candidate for clinical study with oncological PH, but one that carries the risk of overexposure in the early postoperative phase.
Evaluation of the Effect of Four Fibers on Laxation, Gastrointestinal Tolerance and Serum Markers in Healthy Humans
Authors: Stewart Maria L. , Nikhanj Soma D. , Timm Derek A. , Thomas William , Slavin Joanne L.
Published: January 2010

Background: Average dietary fiber intake in the United States is roughly half of the recommended amount. As new dietary fiber products are introduced to increase fiber intake, it is critical to evaluate the physiological effects of such fibers. Aims: This study examined the effect of 4 fibers derived from maize or tapioca on fecal chemistry, gastrointestinal (GI) symptoms and serum markers of chronic disease. Methods: Twenty healthy subjects completed the single-blind crossover study in which 12 g/day of fiber (pullulan, Promitor™ Resistant Starch, soluble fiber dextrin or Promitor Soluble Corn Fiber) or placebo (maltodextrin) were consumed for 14 days followed by a 21-day washout. GI symptom surveys were completed (days 3 and 14), stools were collected (days 11–14), diet was recorded (days 12–14) and fasting blood samples were obtained (day 15). Results: The 4 test fibers were well tolerated, with mild to moderate GI symptoms. Total short-chain fatty acid (SCFA) concentrations did not differ among the treatments. Fecal pH and individual SCFAs were affected by some treatments. Stool weight and serum markers of chronic disease did not change with these treatments. Conclusion: Increasing fiber intake by 12 g/day was well tolerated and may have a positive impact on colon health due to fermentation.
Failure of Postnatal Ductus Arteriosus Closure in Prostaglandin Transporter–Deficient Mice
Authors: Chang Hee-Yoon , Locker Joseph , Lu Run , Schuster Victor L.
Published: January 2010

Background—Prostaglandin E2(PGE2) plays a major role both in maintaining patency of the fetal ductus arteriosus and in closure of the ductus arteriosus after birth. The rate-limiting step in PGE2signal termination is PGE2uptake by the transporter PGT.

Methods and Results—To determine the role of PGT in ductus arteriosus closure, we used a gene-targeting strategy to produce mice in which PGT exon 1 was flanked by loxP sites. Successful targeting was obtained because neither mice hypomorphic at the PGT allele (PGT Neo/Neo) nor global PGT knockout mice (PGT−/−) exhibited PGT protein expression; moreover, embryonic fibroblasts isolated from targeted mice failed to exhibit carrier-mediated PGE2uptake. Although born in a normal mendelian ratio, no PGT−/−mice survived past postnatal day 1, and no PGT Neo/Neo mice survived past postnatal day 2. Necropsy revealed patent ductus arteriosus with normal intimal thickening but dilated cardiac chambers. Both PGT Neo/Neo and PGT−/−mice could be rescued through the postnatal period by giving the mother indomethacin before birth. Rescued mice grew normally and had no abnormalities by gross and microscopic postmortem analyses. In accordance with the known role of PGT in metabolizing PGE2, rescued adult PGT−/−mice had lower plasma PGE2metabolite levels and higher urinary PGE2excretion rates than wild-type mice.

Conclusion—PGT plays a critical role in closure of the ductus arteriosus after birth by ensuring a reduction in local and/or circulating PGE2concentrations.
Cytochrome 2C19*17 Allelic Variant, Platelet Aggregation, Bleeding Events, and Stent Thrombosis in Clopidogrel-Treated Patients With Coronary Stent Placement
Authors: Sibbing Dirk , Koch Werner , Gebhard Daniela , Schuster Tibor , Braun Siegmund , Stegherr Julia , Morath Tanja , Schömig Albert , von Beckerath Nicolas , Kastrati Adnan
Published: January 2010

Background—

The cytochrome P450 (CYP) 2C19 isoenzyme plays an important role in clopidogrel metabolization. A recently explored
CYP2C19
*
17
allelic variant has been linked to increased transcriptional activity, resulting in extensive metabolization of
CYP2C19
substrates, which may lead to an enhanced platelet response to clopidogrel treatment. The aim of this study was to assess the impact of
CYP2C19
*
17
on ADP-induced platelet aggregation, the risk of bleeding, and stent thrombosis in clopidogrel-treated patients undergoing percutaneous coronary intervention.

Methods and Results—

The study population included 1524 patients undergoing percutaneous coronary intervention after pretreatment with 600 mg clopidogrel. Genotypes were determined with a TaqMan assay. ADP-induced platelet aggregation was assessed on a Multiplate analyzer. The primary clinical safety end point was the 30-day incidence of bleeding defined according to Thrombolysis in Myocardial Infarction criteria, and the primary clinical efficacy end point was the 30-day incidence of stent thrombosis. For both heterozygous (*wt/*17; n=546) and homozygous (*17/*17; n=76) allele carriers, significantly lower ADP-induced platelet aggregation values were found compared with wild-type homozygotes (*wt/*wt; n=902;
P
=0.039 and
P
=0.008, respectively).
CYP2C19
*
17
allele carriage was significantly associated with an increased risk of bleeding; the highest risk was observed for
CYP2C19
*
17
homozygous patients (
P
=0.01, χ
2
test for trend). Multivariate analysis confirmed the independent association of
CYP2C19
*
17
allele carriage with platelet aggregation values (
P
<0.001) and the occurrence of bleeding (
P
=0.006). No significant influence of
CYP2C19
*
17
on the occurrence of stent thrombosis was found (
P
=0.79).

Conclusions—

CYP2C19
*
17
carrier status is significantly associated with enhanced response to clopidogrel and an increased risk of bleeding.
Bibliotheca frisica juridica III Bio-bibliografische notities over enkele weinig bekende Friese juristen Bibliotheca Frisica juridica III, Bio-bibliographical notes on some little known Frisian jurists
Authors: Feenstra R.
Published: January 2010

Third part of a series on some early Frisian jurists who have left printed editions of their works (for the first part see TR 75 (2007), p. 125–137, for the second part see TR 76 (2008), p. 329–351). The present contribution deals with Franciscus Meinardus (1569/1570–1623), teaching as a licentiatus in Angers and professor in Poitiers, and with Dominicus Arumaeus (1579–1637), professor in Jena and one of the founders of the German science of public law. At the end some corrections and additions regarding the notes on Haring Sinnema (in part I), Joachimus Hopperus (in part II) and Thomas Herbaius (also in part II).
Hugo Grotius and the Thirty Years War, An early reception of De iure belli ac pacis
Authors: Müller Edgar
Published: January 2010

It is generally assumed that the peace negotiations at Münster and Osnabrück were influenced by the Spanish authors of the so-called Second Scholastics such as Francisco Suarez and Francisco de Vitoria, although evidence of that influence is lacking. It is possible, however, to establish that Grotius's book on the law of war and peace did influence the Westphalian negotiations. De iure belli et pacis was first published in 1625; it was widely read and during the 1630s it was used for teaching purposes in the universities of Strasbourg, Tübingen, Ingolstadt and Uppsala.