Observation of an Antimatter Hypernucleus

Nuclear collisions recreate conditions in the universe microseconds after the Big Bang. Only a very small fraction of the emitted fragments are light nuclei, but these states are of fundamental interest. We report the observation of antihypertritons-comprising an antiproton, an antineutron, and an antilambda hyperon-produced by colliding gold nuclei at high energy. Our analysis yields 70 +/- 17 antihypertritons (3/Lambda(H) over bar) and 157 +/- 30 hypertritons (H-3(Lambda)). The measured yields of H-3(Lambda) (3/Lambda(H) over bar) and He-3 ((3)(He) over bar) are similar, suggesting an equilibrium in coordinate and momentum space populations of up, down, and strange quarks and antiquarks, unlike the pattern observed at lower collision energies. The production and properties of antinuclei, and of nuclei containing strange quarks, have implications spanning nuclear and particle physics, astrophysics, and cosmology.

Longitudinal scaling property of the charge balance function in Au plus Au collisions at root s(NN)=200 GeV

We present measurements of the charge balance function, from the charged particles, for diverse pseudorapidity and transverse momentum ranges in Au + Au collisions at root S-NN = 200 GeV using the STAR detector at RHIC. We observe that the balance function is boost-invariant within the pseudorapidity coverage vertical bar-1.3, 1.3 vertical bar. The balance function properly scaled by the width of the observed pseudorapidity window does not depend on the position or size of the pseudorapidity window. This scaling property also holds for particles in different transverse momentum ranges. In addition, we find that the width of the balance function decreases monotonically with increasing transverse momentum for all centrality classes. (c) 2010 Elsevier B.V. All rights reserved.

生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。

Type-omega DPLs

Type-omega DPLs (Denotational Proof Languages) are languages for proof presentation and search that offer strong soundness guarantees. LCF-type systems such as HOL offer similar guarantees, but their soundness relies heavily on static type systems. By contrast, DPLs ensure soundness dynamically, through their evaluation semantics; no type system is necessary. This is possible owing to a novel two-tier syntax that separates deductions from computations, and to the abstraction of assumption bases, which is factored into the semantics of the language and allows for sound evaluation. Every type-omega DPL properly contains a type-alpha DPL, which can be used to present proofs in a lucid and detailed form, exclusively in terms of primitive inference rules. Derived inference rules are expressed as user-defined methods, which are "proof recipes" that take arguments and dynamically perform appropriate deductions. Methods arise naturally via parametric abstraction over type-alpha proofs. In that light, the evaluation of a method call can be viewed as a computation that carries out a type-alpha deduction. The type-alpha proof "unwound" by such a method call is called the "certificate" of the call. Certificates can be checked by exceptionally simple type-alpha interpreters, and thus they are useful whenever we wish to minimize our trusted base. Methods are statically closed over lexical environments, but dynamically scoped over assumption bases. They can take other methods as arguments, they can iterate, and they can branch conditionally. These capabilities, in tandem with the bifurcated syntax of type-omega DPLs and their dynamic assumption-base semantics, allow the user to define methods in a style that is disciplined enough to ensure soundness yet fluid enough to permit succinct and perspicuous expression of arbitrarily sophisticated derived inference rules. We demonstrate every major feature of type-omega DPLs by defining and studying NDL-omega, a higher-order, lexically scoped, call-by-value type-omega DPL for classical zero-order natural deduction---a simple choice that allows us to focus on type-omega syntax and semantics rather than on the subtleties of the underlying logic. We start by illustrating how type-alpha DPLs naturally lead to type-omega DPLs by way of abstraction; present the formal syntax and semantics of NDL-omega; prove several results about it, including soundness; give numerous examples of methods; point out connections to the lambda-phi calculus, a very general framework for type-omega DPLs; introduce a notion of computational and deductive cost; define several instrumented interpreters for computing such costs and for generating certificates; explore the use of type-omega DPLs as general programming languages; show that DPLs do not have to be type-less by formulating a static Hindley-Milner polymorphic type system for NDL-omega; discuss some idiosyncrasies of type-omega DPLs such as the potential divergence of proof checking; and compare type-omega DPLs to other approaches to proof presentation and discovery. Finally, a complete implementation of NDL-omega in SML-NJ is given for users who want to run the examples and experiment with the language.

Irańska sztuka a perska archeologia starożytna w czasach Pahlawich (1925-1979)

Wydział Historyczny: Instytut Historii Sztuki

Addresses of Rev. Drs. Park, Post, & Bacon : at the anniversary of the American Congregational Union, May, 1854.

http://www.archive.org/details/addressesofrevdr00parkuoft

History of the Catholic missions among the Indian tribes of the United States, 1529-1854 / by John Gilmary Shea.

http://www.archive.org/details/historyofcatholi00sheaiala

England's mission to India : Some impressions from a recent visit / by Alfred Barry.

http://www.archive.org/details/englandsmissiont00barruoft

Adding Polymorphic Abstraction to ML (Detailed Abstract)

The ML programming language restricts type polymorphism to occur only in the "let-in" construct and requires every occurrence of a formal parameter of a function (a lambda abstraction) to have the same type. Milner in 1978 refers to this restriction (which was adopted to help ML achieve automatic type inference) as a serious limitation. We show that this restriction can be relaxed enough to allow universal polymorphic abstraction without losing automatic type inference. This extension is equivalent to the rank-2 fragment of system F. We precisely characterize the additional program phrases (lambda terms) that can be typed with this extension and we describe typing anomalies both before and after the extension. We discuss how macros may be used to gain some of the power of rank-3 types without losing automatic type inference. We also discuss user-interface problems in how to inform the programmer of the possible types a program phrase may have.

Programming Examples Needing Polymorphic Recursion

Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic recursion using for all-types has been proved undecidable. This report presents several programming examples involving polymorphic recursion and determines their typability under various type systems, including the Hindley-Milner system, an intersection-type system, and extensions of these two. The goal of this report is to show that many of these examples are typable using a system of intersection types as an alternative form of polymorphism. By accomplishing this, we hope to lay the foundation for future research into a decidable intersection-type inference algorithm. We do not provide a comprehensive survey of type systems appropriate for polymorphic recursion, with or without type annotations inserted in the source language. Rather, we focus on examples for which types may be inferred without type annotations.

Safe Compositional Specification of Network Systems With Polymorphic, Constrained Types

In the framework of iBench research project, our previous work created a domain specific language TRAFFIC [6] that facilitates specification, programming, and maintenance of distributed applications over a network. It allows safety property to be formalized in terms of types and subtyping relations. Extending upon our previous work, we add Hindley-Milner style polymorphism [8] with constraints [9] to the type system of TRAFFIC. This allows a programmer to use for-all quantifier to describe types of network components, escalating power and expressiveness of types to a new level that was not possible before with propositional subtyping relations. Furthermore, we design our type system with a pluggable constraint system, so it can adapt to different application needs while maintaining soundness. In this paper, we show the soundness of the type system, which is not syntax-directed but is easier to do typing derivation. We show that there is an equivalent syntax-directed type system, which is what a type checker program would implement to verify the safety of a network flow. This is followed by discussion on several constraint systems: polymorphism with subtyping constraints, Linear Programming, and Constraint Handling Rules (CHR) [3]. Finally, we provide some examples to illustrate workings of these constraint systems.

The multiple reality: A critical study on Alfred Schutz’s sociology of the finite provinces of meaning

This work is a critical introduction to Alfred Schutz’s sociology of the multiple reality and an enterprise that seeks to reassess and reconstruct the Schutzian project. In the first part of the study, I inquire into Schutz’s biographical context that surrounds the germination of this conception and I analyse the main texts of Schutz where he has dealt directly with ‘finite provinces of meaning.’ On the basis of this analysis, I suggest and discuss, in Part II, several solutions to the shortcomings of the theoretical system that Schutz drew upon the sociological problem of multiple reality. Specifically, I discuss problems related to the structure, the dynamics, and the interrelationing of finite provinces of meaning as well as the way they relate to the questions of narrativity, experience, space, time, and identity.

The characterization of twenty sequenced human genomes.

We present the analysis of twenty human genomes to evaluate the prospects for identifying rare functional variants that contribute to a phenotype of interest. We sequenced at high coverage ten "case" genomes from individuals with severe hemophilia A and ten "control" genomes. We summarize the number of genetic variants emerging from a study of this magnitude, and provide a proof of concept for the identification of rare and highly-penetrant functional variants by confirming that the cause of hemophilia A is easily recognizable in this data set. We also show that the number of novel single nucleotide variants (SNVs) discovered per genome seems to stabilize at about 144,000 new variants per genome, after the first 15 individuals have been sequenced. Finally, we find that, on average, each genome carries 165 homozygous protein-truncating or stop loss variants in genes representing a diverse set of pathways.

A fast, streaming SIMD extensions 2, logistic squashing function

Schraudolph proposed an excellent exponential approximation providing increased performance particularly suited to the logistic squashing function used within many neural networking applications. This note applies Intel's streaming SIMD Extensions 2 (SSE2), where SIMD is single instruction multiple data, of the Pentum IV class processor to Schraudolph's technique, further increasing the performance of the logistic squashing function. It was found that the calculation of the new 32-bit SSE2 logistic squashing function described here was up to 38 times faster than the conventional exponential function and up to 16 times faster than a Schraudolph-style 32-bit method on an Intel Pentum D 3.6 GHz CPU.