Male dimorphism of a neotropical arachnid: harem size, sneaker opportunities, and gonadal investment

Serracutisoma proximum is a harvestman with alternative male morphs. Large males use sexually dimorphic second legs in fights for the possession of territories on the vegetation, where females oviposit. Small males have short second legs and do not fight but rather sneak into the territories and copulate with egg-guarding females. We investigated the presence of male dimorphism across 10 populations of S. proximum, compared gonadal investment between male morphs, and assessed if the distribution of the sneakers is influenced by harem size. In all populations, there was male dimorphism, indicated by the bimodal distribution of the leg II length/body length. Gonadal investment did not differ between morphs and was not affected by male size, second leg length, and morph relative frequency in the populations. We found 361 territories, 90.0% containing 1 male, 9.7% containing 2 males (dyads), and 0.3% containing 3 males. The probability of encountering dyads increased with the number of females present in the territories. Moreover, the proportion of sneakers in territories containing dyads was higher than would be expected by chance. One possible reason for the ubiquity of alternative morphs in S. proximum could be the high mating opportunities experienced by sneakers in spatially structured populations with a resource defense polygyny system. Additionally, the high frequency of successful invasions by sneakers and hence the high sperm competition risk for both morphs may explain the similarity in gonadal investment between male morphs.

In Vitro PLK1 Inhibition by BI 2536 Decreases Proliferation and Induces Cell-Cycle Arrest in Melanoma Cells

Melanoma is one of the most treatment-resistant malignancies and regardless of new therapeutic tactics the outcome remains dismal. Polo-like kinase 1 (PLK1) has been shown to be over-expressed in a variety of tumors, becoming an attractive target for cancer management. In the present study we tested the in vitro antitumor activities of BI 2536, a selective inhibitor of PLK1, against two melanoma cell lines. Our results showed that nanomolar concentrations (10-150 nmol/L) of the drug significantly decreased cell proliferation and clonogenicity, promoting cell cycle arrest in G2/M. Targeting the cell cycle offers an attractive potential cancer-treatment option. Herein we show that PLK1 inhibition may be a feasible approach for the impairment of tumor progression and dissemination. This in vitro profile of melanoma cell growth inhibition by PLK1 modulation may be an interesting model to be tested in association with first-line antineoplasic agents in melanomas.

The SB-index and the HSB-index: efficient indices for spatial data warehouses

Spatial data warehouses (SDWs) allow for spatial analysis together with analytical multidimensional queries over huge volumes of data. The challenge is to retrieve data related to ad hoc spatial query windows according to spatial predicates, avoiding the high cost of joining large tables. Therefore, mechanisms to provide efficient query processing over SDWs are essential. In this paper, we propose two efficient indices for SDW: the SB-index and the HSB-index. The proposed indices share the following characteristics. They enable multidimensional queries with spatial predicate for SDW and also support predefined spatial hierarchies. Furthermore, they compute the spatial predicate and transform it into a conventional one, which can be evaluated together with other conventional predicates by accessing a star-join Bitmap index. While the SB-index has a sequential data structure, the HSB-index uses a hierarchical data structure to enable spatial objects clustering and a specialized buffer-pool to decrease the number of disk accesses. The advantages of the SB-index and the HSB-index over the DBMS resources for SDW indexing (i.e. star-join computation and materialized views) were investigated through performance tests, which issued roll-up operations extended with containment and intersection range queries. The performance results showed that improvements ranged from 68% up to 99% over both the star-join computation and the materialized view. Furthermore, the proposed indices proved to be very compact, adding only less than 1% to the storage requirements. Therefore, both the SB-index and the HSB-index are excellent choices for SDW indexing. Choosing between the SB-index and the HSB-index mainly depends on the query selectivity of spatial predicates. While low query selectivity benefits the HSB-index, the SB-index provides better performance for higher query selectivity.

CT-guided percutaneous drilling is a safe and reliable method of treating osteoid osteomas

Computed tomography (CT)-guided percutaneous drilling is an alternative for osteoid osteoma treatment. This study aims to evaluate the remodeling of the drill orifice. The success rate and complications were also recorded and compared with other treatment methods.

Disruption of endogenous tidal rhythms of larval release linked to food supply and heat stress in an intertidal barnacle

The timing of larval release may greatly affect the survivorship and distribution of pelagic stages and reveal important aspects of life history tactics in marine invertebrates. Endogenous rhythms of breeding individuals and populations are valuable indicators of selected strategies because they are free of the neutral effect of stochastic environmental variation. The high-shore intertidal barnacle Chthamalus bisinuatus exhibits endogenous tidal and tidal amplitude rhythms in a way that larval release would more likely occur during fortnightly neap periods at high tide. Such timing would minimize larval loss due to stranding and promote larval retention close to shore. This fully explains temporal patterns in populations facing the open sea and inhabiting eutrophic areas. However, rhythmic activity breaks down to an irregular pattern in a population within the São Sebastião Channel subjected to large variation of food supply around a mesotrophic average. Peaks of chl a concentration precede release events by 6 d, suggesting resource limitation for egg production within the channel. Also, extreme daily temperatures imposing mortality risk correlate to release rate just 1 d ahead, suggesting a terminal reproductive strategy. Oceanographic conditions apparently dictate whether barnacles follow a rhythmic trend of larval release supported by endogenous timing or, alternatively, respond to the stochastic variation of key environmental factors, resulting in an erratic temporal pattern.

Sexual selection in Pomatoschistus – nests, sperm competition, and paternal care

Sexual selection arises through variation in reproductive success. This thesis investigates different aspects important in sexual selection, namely nest building, sperm competition, paternity and paternal care, and their mutual interrelationships. In the studied species, the sand goby (Pomatoschistus minutus) and the common goby (Pomatoschistus microps), sperm competition did arise when small males, so called sneakers, sneaked into other males nests and released sperm. They seemed to use female behaviour as their prime cue for a sneaking opportunity. However, also nest-holders, both with and without eggs, were found to fertilize eggs in the nests of other males. Clearly, nest-holding males tried to prevent other males from spreading their sperm in their nests, since they showed aggression towards such males. A nest building experiment indicated that the small nest-openings found in the sneaker male treatment were sexually selected through protection against sneaking or by female choice. Yet, no behavioural or genetical support for the hypothesis that the nest functions as a physical or visual defence, or that sneaker males prefer to sneak upon nests with wide nest-openings, were found in the other studies. Still, individual nest-holding males showed a higher mucus preparation effort inside the nest in the presence of a sneaker male than when alone. In close relatives, such mucus contains sperm, suggesting an importance in sperm competition. However, the mucus may also have pheromone and anti-bacterial functions and may constitute a mating effort, as found in other gobies. Both a behavioural and a mate choice experiment suggested that the males were not less eager to spawn in the presence of a sneaker male. Sneak intrusion did not affect nest defence, fanning or filial cannibalism, nor had paternity an effect on filial cannibalism. This and various life history aspects, together with the fact that the parasitic male only fertilized a fraction of the clutches, would predict females to ignore sneaker males. This was also the case, as the presence of sneaker males was found not to affect female spawning decision. Still, several females spawned in two nests, which coincided with parasitic spawnings, suggesting a cost of disturbance for the females and thus a substantial cost to the nest-holding males in terms of lost mating success. However, females paid attention to other traits in their choice of mate since spawning was associated with sand volume of the nest, but not with nest-opening width. Also, female (but not male) courtship was correlated with partial clutch filial cannibalism, indicating that females are able to anticipate future male cannibalism. In a partial correlation of nest opening, sand volume, male courtship display, displacement fanning and male size, a large number of traits were correlated both positively and negatively with regard to how we may expect them to be appreciated by females. For instance, males which fan well also build large nests or display intensely (but not both). Together with all the other results of this thesis, this shows the entangled selection pressures working on breeding animals, as well as the different male and female tactics employed to maximize their reproduction.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Mediterranean brachiopods: morphological, ecological and phylogenetic aspects

The Brachiopoda of the Marine Protected Area “Secche di Tor Paterno”, Central Tyrrhenian Sea, have been investigated in order to give a first glance of the diversity of the brachiopods of this area and provide a new report on the Mediterranean Brachiopod fauna. Four species were reported: Novocrania anomala (Müller, 1776), Megathiris detruncata (Gmelin, 1790), Joania cordata (Risso,1826) and Argyrotheca cuneata (Risso,1826). For all the four species a morphological analysis was carried out. For the two most abundant species, J.cordata and A. cuneata, a morphometric study, based on thickness/width and length/width scattergrams, was carried out, in order to investigate their variability. Size-frequency distributions relative to the three dimensions of the shell were also computed, aimed at a evaluation of population dynamics of these two species. The results showed that, for both species, the parameters which most determine the rise of the shell during the growth of animal are width and length and that frequency distributions are mainly bi- or plurymodal and that they are difficult to interpret, as reported by other studies. Analysis of drill holes found on the shell of some specimens of the two same species revealed a predatory origin and that three different predators are responsible for them. Partial sequences of two different genetic markers, the Internal Transcribed Spacer 1 (ITS1) and the cytochrome oxidase subunit 1 (COI), were used to investigate the phylogenetic relationship between two populations of the eurybathic brachiopod species Gryphus vitreus (Born,1778) across the strait of Gibraltar. This represents the first genetic population study on brachiopods. Results from AMOVA and Bayesian analysis performed on 31 specimens highlighted no genetic differentiation indicating a likely panmixia, dispite the lecitotrophic development of the species.

Recycled crustal material in the geochemical record of Pacific ocean island basalts from Pitcairn, Hawaii and Rurutu

Die Isotopenzusammensetzungen des Pitcairn Hotspot (Südpazifik), des Mauna Kea (Hawaii) und der Insel Rurutu (Französisch Polynesien) wurden bestimmt, um Heterogenitäten im Erdmantel zu charakterisieren. Die Bleiisotopenzusammensetzung wurde mit einer Dreiisotopenspiketechnik zur Korrektur der instrumentellen Massenfraktionierung gemessen. An Proben von Pitcairn wurde zusätzlich die Os, Hf, Nd, Sr Isotopenzusammensetzung, sowie die Haupt- und Spurenelementzusammensetzung bestimmt. Die Isotopensignatur des Pitcairn Hotspots kann durch eine Sedimentkomponente in der Magmenquelle erklärt werden. Die Bleiisotopenschwankungen des Mauna Kea in der HSDP-2 Bohrung treten als Oszillationen auf, die sich zu linearen Anordnungen im Bleiisotopenraum zusammensetzen. Das begrenzte zeitliche Auftreten einer linearen Anordnung zeigt, daß die Heterogenitäten mehrere zehner Kilometer Länge im aufsteigenden Mantelmaterial unter dem Vulkan einnehmen. Auch die Bleiisotopenzusammensetzungen der Rurutu-laven zeigen lineare Anordnungen.Diese lineare Anordnungen im Bleiisotopenraum können durch eine vorwiegend binäre Mischung erklärt werden. Ein Bleiisotopenentwicklungsmodell unterstützt, daß die Differenzierung der Ausgangsmaterialien vor weniger als etwa zwei Milliarden Jahren geschah und für Mauna Kea relativ jung sein könnte. Keine der Hotspots weisen identische Mischungsendglieder auf, so daß die Heterogenitäten kleinräumige Merkmale im Erdmantel sind.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

Im/possible Lives: Gender, Class, Self-Fashioning, and Affinal Solidarity in Modern South Asia

Drawing on ethnographic research and employing a micro-historical approach that recognizes not only the transnational but also the culturally specific manifestations of modernity, this article centers on the efforts of a young woman to negotiate shifting and conflicting discourses about what a good life might consist of for a highly educated and high caste Hindu woman living at the margins of a nonetheless globalized world. Newly imaginable worlds in contemporary Mithila,South Asia, structure feeling and action in particularly gendered and classed ways, even as the capacity of individuals to actualize those worlds and the “modern” selves envisioned within them are constrained by both overt and subtle means. In the context of shifting cultural anchors, new practices of silence, literacy, and even behaviors interpreted as “mental illness” may become tactics in an individual’s negotiation of conflicting self-representations. The confluence of forces at play in contemporary Mithila, moreover, is creating new structures of feeling that may begin to reverse long-standing locally held assumptions about strong solidarities between natal families and daughters, on the one hand, and weak solidarities between affinal families and new daughters-in-law, on the other.

"Security Here is Not Safe": Violence, Punishment, and Space in the Contemporary US Penitentiary

The US penitentiary at Lewisburg, Pennsylvania, was retrofitted in 2008 to offer the country's first federal Special Management Unit (SMU) program of its kind. This model SMU is designed for federal inmates from around the country identified as the most intractably troublesome, and features double-celling of inmates in tiny spaces, in 23-hour or 24-hour a day lockdown, requiring them to pass through a two-year program of readjustment. These spatial tactics, and the philosophy of punishment underlying them, contrast with the modern reform ideals upon which the prison was designed and built in 1932. The SMU represents the latest punitive phase in American penology, one that neither simply eliminates men as in the premodern spectacle, nor creates the docile, rehabilitated bodies of the modern panopticon; rather, it is a late-modern structure that produces only fear, terror, violence, and death. This SMU represents the latest of the late-modern prisons, similar to other supermax facilities in the US but offering its own unique system of punishment as well. While the prison exists within the system of American law and jurisprudence, it also manifests features of Agamben's lawless, camp-like space that emerges during a state of exception, exempt from outside scrutiny with inmate treatment typically beyond the scope of the law

Comparison of implant stability by means of resonance frequency analysis for flapless and conventionally inserted implants

Background: Resonance frequency analysis (RFA) is a noninvasive technique for the quantitative assessment of implant stability. Information on the implant stability quotient (ISQ) of transmucosally inserted implants is limited. Purpose: The aim of this investigation was to compare the ISQ of conventionally inserted implants by raising a muco-periostal flap with implants inserted using a flapless procedure. Materials and Methods: Forty elderly patients with complete edentulous maxilla were consecutively admitted for treatment with implant-supported prostheses. A computer tomography was obtained for the computer-assisted implant planning. One hundred ten implants were placed conventionally in 23 patients (flap-group) and 85 implants in 17 patients by means of the flapless method (flapless-group) using a stereolithographic template. RFA measurements were performed after implant placement (baseline) and after a healing time of 12 weeks (reentry). Results: All implants exhibited clinically and radiographically successful osseointegration. Bone level did not change significantly neither for genders nor type of surgical protocol. Mean ISQ values of the flapless-group were significantly higher at baseline (p < .001) and at reentry (p < .001) compared with the flap-group. The ISQ values were significantly lower at reentry compared with baseline for the flap-group (p = .028) but not for the flapless-group. This group showed a moderate, but insignificant increase. RFA measurements of males resulted in ISQ values that were thoroughly higher as compared with females at both time-points in both groups. Correlation between RFA and bone level was not found. Conclusions: The flapless procedure showed favorable conditions with regard to implant stability and crestal bone level. Some changes of the ISQ values that represent primary (mechanical) and secondary (bone remodeling) implant stability were observed in slight favor of the flapless method and male patients. In properly planned and well-selected cases, the minimal invasive transmucosal technique using a drill-guide is a safe procedure.

Where Stories Collide : Montage and the Short Story Cycle

This thesis uses Sergei Eisenstein’s filmic theories of montage to examine the modernist American short story cycle, a genre of independent short stories that work together to create a larger and interrelated whole. Similar to the shot-by-shot editing process of montage, the story cycle builds its intertextual meaning story-by-story from an aggregate of abrupt narrative transitions and juxtapositions. Eisenstein famously felt that montage, the editing together of film fragments, was not a process of linkage, but of collision –each radically different shot in a film should crash into the next shot, until audience members were intellectually provoked into synthesizing these collisions through dialectical processes. I offer montage as an interpretive strategy for negotiating the narrative collisions in story cycles such as Sherwood Anderson’s Winesburg, Ohio, William Faulkner’s Go Down, Moses, and Eudora Welty’s The Golden Apples. For Go Down, Moses, I argue that Eisenstein’s politically rendered “montage of attractions” provides a template for investigating the shock tactics behind Faulkner’s chronologically and racially entangled stories of whites and African Americans. For The Golden Apples, I consider the opposites and doubles in Welty’s fiction with Eisenstein’s similar belief in the “opposing passions” of the world. Not only, then, do I suggest that the modernist story cycle bears a cinematic influence, but I also offer Eisenstein’s theories of montage and collision as a heuristic for formal, thematic, and even political patterns in a genre infamous for its resistance to definition and classification.

Using Micro-Gravity Techniques to Map Alluvium Thickness and Pleistocene Location of the West Branch of the Susquehanna River Near Muncy, Pennsylvania

Laurentide glaciation during the early Pleistocene (~970 ka) dammed the southeast-flowing West Branch of the Susquehanna River (WBSR), scouring bedrock and creating 100-km-long glacial Lake Lesley near the Great Bend at Muncy, Pennsylvania (Ramage et al., 1998). Local drill logs and well data indicate that subsequent paleo-outwash floods and modern fluvial processes have deposited as much as 30 meters of alluvium in this area, but little is known about the valley fill architecture and the bedrock-alluvium interface. By gaining a greater understanding of the bedrock-alluvium interface the project will not only supplement existing depth to bedrock information, but also provide information pertinent to the evolution of the Muncy Valley landscape. This project determined if variations in the thickness of the valley fill were detectable using micro-gravity techniques to map the bedrock-alluvium interface. The gravity method was deemed appropriate due to scale of the study area (~30 km2), ease of operation by a single person, and the available geophysical equipment. A LaCoste and Romberg Gravitron unit was used to collect gravitational field readings at 49 locations over 5 transects across the Muncy Creek and Susquehanna River valleys (approximately 30 km2), with at least two gravity base stations per transect. Precise latitude, longitude and ground surface elevation at each location were measured using an OPUS corrected Trimble RTK-GPS unit. Base stations were chosen based on ease of access due to the necessity of repeat measurements. Gravity measurement locations were selected and marked to provide easy access and repeat measurements. The gravimeter was returned to a base station within every two hours and a looping procedure was used to determine drift and maximize confidence in the gravity measurements. A two-minute calibration reading at each station was used to minimize any tares in the data. The Gravitron digitally recorded finite impulse response filtered gravity measurements every 20 seconds at each station. A measurement period of 15 minutes was used for each base station occupation and a minimum of 5 minutes at all other locations. Longer or multiple measurements were utilized at some sites if drift or other externalities (i.e. train or truck traffic) were effecting readings. Average, median, standard deviation and 95% confidence interval were calculated for each station. Tidal, drift, latitude, free-air, Bouguer and terrain corrections were then applied. The results show that the gravitational field decreases as alluvium thickness increases across the axes of the Susquehanna River and Muncy Creek valleys. However, the location of the gravity low does not correspond with the present-day location of the West Branch of the Susquehanna River (WBSR), suggesting that the WBSR may have been constrained along Bald Eagle Mountain by a glacial lobe originating from the Muncy Creek Valley to the northeast. Using a 3-D inversion model, the topography of the bedrock-alluvium interface was determined over the extent of the study area using a density contrast of -0.8 g/cm3. Our results are consistent with the bedrock geometry of the area, and provide a low-cost, non-invasive and efficient method for exploring the subsurface and for supplementing existing well data.