bluuebunny/crossref_metadata_2025_split huggingface dataset:
Bringing extensibility to verified compilers
Authors: Tatlock Zachary , Lerner Sorin 
Published: June 2010

Verified compilers, such as Leroy's CompCert, are accompanied by a fully checked correctness proof. Both the compiler and proof are often constructed with an interactive proof assistant. This technique provides a strong, end-to-end correctness guarantee on top of a small trusted computing base. Unfortunately, these compilers are also challenging to extend since each additional transformation must be proven correct in full formal detail.
At the other end of the spectrum, techniques for compiler correctness based on a domain-specific language for writing optimizations, such as Lerner's Rhodium and Cobalt, make the compiler easy to extend: the correctness of additional transformations can be checked completely automatically. Unfortunately, these systems provide a weaker guarantee since their end-to-end correctness has not been proven fully formally.
We present an approach for compiler correctness that provides the best of both worlds by bridging the gap between compiler verification and compiler extensibility. In particular, we have extended Leroy's CompCert compiler with an execution engine for optimizations written in a domain specific and proved that this execution engine preserves program semantics, using the Coq proof assistant. We present our CompCert extension, XCert, including the details of its execution engine and proof of correctness in Coq. Furthermore, we report on the important lessons learned for making the proof development manageable.
Printing floating-point numbers quickly and accurately with integers
Authors: Loitsch Florian 
Published: June 2010

We present algorithms for accurately converting floating-point numbers to decimal representation. They are fast (up to 4 times faster than commonly used algorithms that use high-precision integers) and correct: any printed number will evaluate to the same number, when read again.
Our algorithms are fast, because they require only fixed-size integer arithmetic. The sole requirement for the integer type is that it has at least two more bits than the significand of the floating-point number. Hence, for IEEE 754 double-precision numbers (having a 53-bit significand) an integer type with 55 bits is sufficient. Moreover we show how to exploit additional bits to improve the generated output.
We present three algorithms with different properties: the first algorithm is the most basic one, and does not take advantage of any extra bits. It simply shows how to perform the binary-to-decimal transformation with the minimal number of bits. Our second algorithm improves on the first one by using the additional bits to produce a shorter (often the shortest) result.
Finally we propose a third version that can be used when the shortest output is a requirement. The last algorithm either produces optimal decimal representations (with respect to shortness and rounding) or rejects its input. For IEEE 754 double-precision numbers and 64-bit integers roughly 99.4% of all numbers can be processed efficiently. The remaining 0.6% are rejected and need to be printed by a slower complete algorithm.
Smooth interpretation
Authors: Chaudhuri Swarat , Solar-Lezama Armando 
Published: June 2010

We presentsmooth interpretation, a method to systematically approximate numerical imperative programs by smooth mathematical functions. This approximation facilitates the use of numerical search techniques like gradient descent for program analysis and synthesis. The method extends to programs the notion ofGaussian smoothing, a popular signal-processing technique that filters out noise and discontinuities from a signal by taking its convolution with a Gaussian function.In our setting, Gaussian smoothing executes a program according to a probabilistic semantics; the execution of programPon an inputxafter Gaussian smoothing can be summarized as follows: (1) Apply a Gaussian perturbation tox-- the perturbed input is a random variable following a normal distribution with meanx. (2) Compute and return theexpected outputofPon this perturbed input. Computing the expectation explicitly would require the execution ofPon all possible inputs, but smooth interpretation bypasses this requirement by using a form of symbolic execution to approximate the effect of Gaussian smoothing onP. The result is an efficient but approximate implementation of Gaussian smoothing of programs.Smooth interpretation has the effect of attenuating features of a program that impede numerical searches of its input space -- for example, discontinuities resulting from conditional branches are replaced by continuous transitions. We apply smooth interpretation to the problem of synthesizing values of numerical control parameters in embedded control applications. This problem is naturally formulated as one of numerical optimization: the goal is to find parameter values that minimize the error between the resulting program and a programmer-provided behavioral specification. Solving this problem by directly applying numerical optimization techniques is often impractical due to the discontinuities in the error function. By eliminating these discontinuities, smooth interpretation makes it possible to search the parameter space efficiently by means of simple gradient descent. Our experiments demonstrate the value of this strategy in synthesizing parameters for several challenging programs, including models of an automated gear shift and a PID controller.
Type-preserving compilation of end-to-end verification of security enforcement
Authors: Chen Juan , Chugh Ravi , Swamy Nikhil 
Published: June 2010

A number of programming languages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. Others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must be further compiled to an executable form. A language suitable for source programming backed by a compiler that enables end-to-end verification is missing.
In this paper, we present a type-preserving compiler that translates programs written in FINE, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate Language. FINE is type checked using an external SMT solver to reduce the proof burden on source programmers. We extract explicit LCF-style proof terms from the solver and carry these proof terms in the compilation to DCIL, thereby removing the solver from the trusted computing base. Explicit proofs enable DCIL to be used in a number of important scenarios, including the verification of mobile code, proof-carrying authorization, and evidence-based auditing. We report on our experience using FINE to build reference monitors for several applications, ranging from a plugin-based email client to a conference management server.
Mixing type checking and symbolic execution
Authors: Khoo Yit Phang , Chang Bor-Yuh Evan , Foster Jeffrey S. 
Published: June 2010

Static analysis designers must carefully balance precision and efficiency. In our experience, many static analysis tools are built around an elegant, core algorithm, but that algorithm is then extensively tweaked to add just enough precision for the coding idioms seen in practice, without sacrificing too much efficiency. There are several downsides to adding precision in this way: the tool's implementation becomes much more complicated; it can be hard for an end-user to interpret the tool's results; and as software systems vary tremendously in their coding styles, it may require significant algorithmic engineering to enhance a tool to perform well in a particular software domain.
In this paper, we present Mix, a novel system that mixes type checking and symbolic execution. The key aspect of our approach is that these analyses are applied independently on disjoint parts of the program, in an off-the-shelf manner. At the boundaries between nested type checked and symbolically executed code regions, we use special mix rules to communicate information between the off-the-shelf systems. The resulting mixture is a provably sound analysis that is more precise than type checking alone and more efficient than exclusive symbolic execution. In addition, we also describe a prototype implementation, Mixy, for C. Mixy checks for potential null dereferences by mixing a null/non-null type qualifier inference system with a symbolic executor.
Plasma Cytokines and Future Risk of Non-Hodgkin Lymphoma (NHL): A Case-Control Study Nested in the Italian European Prospective Investigation into Cancer and Nutrition
Authors: Saberi Hosnijeh Fatemeh , Krop Esmeralda J.M. , Scoccianti Chiara , Krogh Vittorio , Palli Domenico , Panico Salvatore , Tumino Rosario , Sacredote Carlotta , Nawroly Niga , Portengen Lützen , Linseisen Jakob , Vineis Paolo , Vermeulen Roel 
Published: June 2010

AbstractBackground: Recently, biological markers related to the immune system such as cytokines have been studied to further understand the etiology of non-Hodgkin Lymphoma (NHL). However, to date, there are no studies that have studied cytokine levels prospectively in relation to NHL risk in the general population.Methods: Using bead-based immunoassays, plasma levels of 11 cytokines, 4 chemokines, and 1 adhesion molecules were measured in prediagnostic blood samples of 86 NHL cases and 86 matched controls (average time between blood collection and diagnosis, 4.5 y). Conditional logistic regression adjusted for body mass index and alcohol consumption was used to analyze the association between individual plasma cytokine levels and the risk of developing NHL.Results: In multivariate models, excluding cases diagnosed within 2 years after inclusion, we observed a significant association for interleukin 2 (IL2; P trend = 0.004), interferon (IFN)-γ (P trend = 0.05), and intercellular adhesion molecule (ICAM) (P trend = 0.04). Subanalyses of B-cell NHL patients showed a significant association with IL2 (P trend = 0.003), tumor necrosis factor-α (TNF-α; P trend = 0.03), and ICAM (P trend = 0.04) and a borderline association with IL5 (P trend = 0.07) and IFN-γ (P trend = 0.08).Conclusions: The results of this study suggest, in a prospective setting, a possible association between plasma levels of IL2, ICAM, IFN-γ, and TNF-α with NHL risk and provide some evidence that risk of NHL might be related to a downregulation of T helper 1 cytokines.Impact: Identification of subtle changes in immune response regulation quantified by plasma cytokine levels possibly provides new insights in the etiology of NHL. Cancer Epidemiol Biomarkers Prev; 19(6); 1577–84. ©2010 AACR.
Adolescent Diet and Subsequent Serum Hormones, Breast Density, and Bone Mineral Density in Young Women: Results of the Dietary Intervention Study in Children Follow-up Study
Authors: Dorgan Joanne F. , Liu Lea , Klifa Catherine , Hylton Nola , Shepherd John A. , Stanczyk Frank Z. , Snetselaar Linda G. , Van Horn Linda , Stevens Victor J. , Robson Alan , Kwiterovich Peter O. , Lasser Norman L. , Himes John H. , Pettee Gabriel Kelley , Kriska Andrea , Ruder Elizabeth H. , Fang Carolyn Y. , Barton Bruce A. 
Published: June 2010

Abstract
Background: Adolescent diet is hypothesized to influence breast cancer risk. We evaluated the long-term effects of an intervention to lower fat intake among adolescent girls on biomarkers that are related to breast cancer risk in adults.
Methods: A follow-up study was conducted on 230 girls who participated in the Dietary Intervention Study in Children (DISC), in which healthy, prepubertal, 8 to 10 year olds were randomly assigned to usual care or to a behavioral intervention that promoted a reduced fat diet. Participants were 25 to 29 years old at follow-up visits. All tests of statistical significance are two-sided.
Results: In analyses that did not take account of diet at the time of the follow-up visit, the only statistically significant treatment group difference was higher bone mineral content in intervention group participants compared with usual care group participants; their mean bone mineral contents were 2,444 and 2,377 g, respectively. After adjustment for current diet, the intervention group also had statistically significantly higher bone mineral density and luteal phase serum estradiol concentrations. Serum progesterone concentrations and breast density did not differ by treatment group in unadjusted or adjusted analyses.
Conclusions: Results do not support the hypothesis that consumption of a lower fat diet during adolescence reduces breast cancer risk via effects on subsequent serum estradiol and progesterone levels, breast density, or bone mineral density. It remains unclear, however, if the results are specific to the DISC intervention or are more broadly applicable.
Impact: Modest reductions in fat intake during adolescence are unlikely to lower later breast cancer risk via long-term effects on the biomarkers measured. Cancer Epidemiol Biomarkers Prev; 19(6); 1545–56. ©2010 AACR.
Chlamydia pneumoniaeInfection and Risk for Lung Cancer
Authors: Chaturvedi Anil K. , Gaydos Charlotte A. , Agreda Patricia , Holden Jeffrey P. , Chatterjee Nilanjan , Goedert James J. , Caporaso Neil E. , Engels Eric A. 
Published: June 2010

AbstractBackground: We evaluated the relationship of Chlamydia pneumoniae infection with prospective lung cancer risk using traditional serologic markers [microimmunoflourescence (MIF) IgG and IgA antibodies] and Chlamydia heat shock protein-60 (CHSP-60) antibodies, a marker for chronic chlamydial infection.Methods: We conducted a nested case-control study (593 lung cancers and 671 controls) within the screening arm of the Prostate, Lung, Colorectal, and Ovarian Cancer Screening Trial (N = 77,464). Controls were matched to cases by age, sex, randomization year, follow-up time, and smoking (pack-years of smoking, time since quitting). We assessed C. pneumoniae seropositivity and endpoint antibody titers (IgG and IgA against C. pneumoniae elementary bodies and IgG against CHSP-60).Results: C. pneumoniae seropositivity by microimmunoflourescence IgG or IgA antibodies was not associated with lung cancer [odds ratio of 0.88 and 95% confidence interval (95% CI) of 0.69-1.13 for IgG; odds ratio of 0.98 and 95% CI of 0.75-1.27 for IgA]. In contrast, individuals seropositive for CHSP-60 IgG antibodies had significantly increased lung cancer risk (odds ratio, 1.30; 95% CI, 1.02-1.67), and risk increased with increasing antibody titers (P trend = 0.006). CHSP-60–related risk did not differ significantly by lung cancer histology, follow-up time, or smoking. CHSP-60 seropositivity was associated with increased risk 2 to 5 years before lung cancer diagnosis (odds ratio, 1.77; 95% CI, 1.16-2.71; P trend = 0.006), thus arguing against reverse causality.Conclusions: CHSP-60 seropositivity and elevated antibody titers were associated with significantly increased risk for subsequent lung cancer, supporting an etiologic role for C. pneumoniae infection in lung carcinogenesis.Impact: Our results highlight the potential for lung cancer risk reduction through treatments targeted toward C. pneumoniae infections and chronic pulmonary inflammation. Cancer Epidemiol Biomarkers Prev; 19(6); 1498–505. ©2010 AACR.
Epidemiology of Extracutaneous Melanoma in the Netherlands
Authors: Koomen Els R. , de Vries Esther , van Kempen Leon C. , van Akkooi Alexander C.J. , Guchelaar Henk Jan , Louwman Marieke W.J. , Nijsten Tamar , Coebergh Jan-Willem W. 
Published: June 2010

Abstract
Background: Reliable population-based incidence and survival data on extracutaneous melanoma (ECM) are sparse.
Methods: Incidence data (1989-2006) from the Netherlands Cancer Registry were combined with vital status on January 1, 2008. Age-adjusted annual incidence rates were calculated by direct standardization, and the estimated annual percentage change was estimated to detect changing trends in incidence. Additionally, we carried out cohort-based relative survival analysis.
Results: Ocular melanomas were the most common ECM subsite with European standardized incidence rates (ESR) of 10.7 and 8.2 per 1,000,000 person-years for males and females, respectively. In comparison, for cutaneous melanoma (CM), the ESRs for men and women were 122 and 155 per million person-years, respectively. No statistically significant trends in the incidence of ECM were detected, whereas an annual increase of 4.4% for men and 3.6% for women was detected in the incidence of CM. Relative survival for ECM was poor, but differed largely between anatomic subtypes ranging from a 5-year relative survival of 74% for ocular melanomas to 15% for certain subsites of mucosal melanomas.
Conclusions: Of all ECM subsites, ocular melanomas had the highest incidence and the best survival. Mucosal melanomas were the second most frequent subsite of ECM. Five-year relative survival for all ECM subtypes was worse if compared with CM. No statistically significant trends in the incidence of (subsites of) ECM were determined.
Impact: This study gives insight into the relative sizes of the different subgroups of ECM as well as an estimate of 5-year survival, which varies substantially by subsite. Cancer Epidemiol Biomarkers Prev; 19(6); 1453–9. ©2010 AACR.
Spatial Patterns of Localized-Stage Prostate Cancer Incidence Among White and Black Men in the Southeastern United States, 1999-2001
Authors: Altekruse Sean F. , Huang Lan , Cucinelli James E. , McNeel Timothy S. , Wells Kristen M. , Oliver M. Norman 
Published: June 2010

Abstract
Background: In the United States, prostate cancer incidence is higher among black than among white males, with a higher proportion of blacks diagnosed with advanced-stage cancer.
Methods: Prostate cancer incidence (1999-2001) and census tract data were obtained for 66,468 cases in four states that account for 20% of U.S. blacks: Georgia, Florida, Alabama, and Tennessee. Spatial clusters of localized-stage prostate cancer incidence were detected by spatial scan. Clusters were examined by relative risk, population density, and socioeconomic and racial attributes.
Results: Overall prostate cancer incidence rates were higher in black than in white men, and a lower proportion of black cases were diagnosed with localized-stage cancer. Strong associations were seen between urban residence and high relative risk of localized-stage cancer. The highest relative risks generally occurred in clusters with a lower percent black population than the national average. Conversely, of eight nonurban clusters with significantly elevated relative risk of localized-disease, seven had a higher proportion of blacks than the national average. Furthermore, positive correlations between percent black population and relative risk of localized-stage cancer were seen in Alabama and Georgia.
Conclusion: Association between urban residence and high relative risk of localized-stage disease (favorable prognosis) persisted after spatial clusters were stratified by percent black population. Unexpectedly, seven of eight nonurban clusters with high relative risk of localized-stage disease had a higher percentage of blacks than the U.S. population.
Impact: Although evidence of racial disparity in prostate cancer was found, there were some encouraging findings. Studies of community-level factors that might contribute to these findings are recommended. Cancer Epidemiol Biomarkers Prev; 19(6); 1460–7. ©2010 AACR.
Low-Penetrance Susceptibility Variants in Familial Colorectal Cancer
Authors: Niittymäki Iina , Kaasinen Eevi , Tuupanen Sari , Karhu Auli , Järvinen Heikki , Mecklin Jukka-Pekka , Tomlinson Ian P.M. , Di Bernardo Maria Chiara , Houlston Richard S. , Aaltonen Lauri A. 
Published: June 2010

Abstract
Background: Genomewide association studies have identified 10 low-penetrance loci that confer modestly increased risk for colorectal cancer (CRC). Although they underlie a significant proportion of CRC in the general population, their impact on the familial risk for CRC has yet to be formally enumerated. The aim of this study was to examine the combined contribution of the 10 variants, rs6983267, rs4779584, rs4939827, rs16892766, rs10795668, rs3802842, rs4444235, rs9929218, rs10411210, and rs961253, on familial CRC.
Methods: The population-based series of CRC samples included in this study consisted of 97 familial cases and 691 sporadic cases. Genotypes in the 10 loci and clinical data, including family history of cancer verified from the Finnish Cancer Registry, were available. The overall number of risk alleles (0-20) was determined, and its association with familial CRC was analyzed. Excess familial risk was estimated using cancer incidence data from the first-degree relatives of the cases.
Results: A linear association between the number of risk alleles and familial CRC was observed (P = 0.006). With each risk-allele addition, the odds of having an affected first-degree relative increased by 1.16 (95% confidence interval, 1.04-1.30). The 10 low-penetrance loci collectively explain ∼9% of the variance in familial risk for CRC.
Conclusions: This study provides evidence to support the previous indirect estimations that these low-penetrance variants account for a relatively small proportion of the familial aggregation of CRC.
Impact: Our results emphasize the need to characterize the remaining molecular basis of familial CRC, which should eventually yield in individualized targeting of preventive interventions. Cancer Epidemiol Biomarkers Prev; 19(6); 1478–83. ©2010 AACR.
Occupational Exposure to Silica and Lung Cancer: Pooled Analysis of Two Case-Control Studies in Montreal, Canada
Authors: Vida Stephen , Pintos Javier , Parent Marie-Élise , Lavoué Jerome , Siemiatycki Jack 
Published: June 2010

Abstract
Background: Respirable crystalline silica is a highly prevalent occupational exposure and a recognized lung carcinogen. Most previous studies have focused on selected high-exposure occupational groups. This study examines the relationship between occupational exposure to silica and lung cancer in an occupationally diverse male population.
Methods: Two large population-based case-control studies of lung cancer were conducted in Montreal, one in 1979-1986 (857 cases, 533 population controls, 1,349 cancer controls) and the second in 1996-2001 (738 cases and 899 controls). Interviews provided descriptive lifetime job histories, smoking histories, and other information. Industrial hygienists translated job histories into histories of exposure to a host of occupational substances, including silica. Relative risk was estimated, adjusting for several potential confounders, including smoking.
Results: The odds ratio for substantial exposure to silica was 1.67 (95% confidence interval, 1.21-2.31) and for any exposure was 1.31 (95% confidence interval, 1.08-1.59). Joint effects between silica and smoking were between additive and multiplicative, perhaps closer to the latter. In this population, it is estimated that approximately 3% of lung cancers were attributable to substantial silica exposure.
Conclusions: The carcinogenicity of inhaled crystalline silica was observed in a population with a wide variety of exposure circumstances.
Impact: The finding of carcinogenicity across a wide range of occupations complements prior studies of specific high-exposure occupations. This suggests that the burden of cancer induced by silica may be much greater than previously thought. Cancer Epidemiol Biomarkers Prev; 19(6); 1602–11. ©2010 AACR.