Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki's banker's queue, and the implicit queue. We formally prove that the banker's queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.
Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to non-federal websites. Their policies may differ from this site.
-
more » « lessFree, publicly-accessible full text available August 15, 2025
-
The investigation of gene regulation therapeutics for the treatment of skin‐related diseases is rarely explored in part due to inefficient systemic delivery. In this study, a bottlebrush polymer‐antisense oligonucleotide (ASO) conjugate, termed pacDNA, designed to target IL‐17 receptor A (IL‐17RA), which is involved in psoriasis pathogenesis is presented. Systemic administration of pacDNA led to its accumulation in epidermis, dermis, and hypodermis of mouse skin, reduced IL‐17RA gene expression in skin, and significantly reversed the development of imiquimod (IMQ)‐induced psoriasis in a mouse model. These findings highlight the potential of the pacDNA as a promising nanoconstruct for systemic oligonucleotide delivery to the skin and for treating psoriasis and other skin‐related disorders through systemic administration.more » « lessFree, publicly-accessible full text available August 14, 2025
-
This study addresses COVID-19 testing as a nonlinear sampling problem, aiming to uncover the dependence of the true infection count in the population on COVID-19 testing metrics such as testing volume and positivity rates. Employing an artificial neural network, we explore the relationship among daily confirmed case counts, testing data, population statistics, and the actual daily case count. The trained artificial neural network undergoes testing in in-sample, out-of-sample, and several hypothetical scenarios. A substantial focus of this paper lies in the estimation of the daily true case count, which serves as the output set of our training process. To achieve this, we implement a regularized backcasting technique that utilizes death counts and the infection fatality ratio (IFR), as the death statistics and serological surveys (providing the IFR) as more reliable COVID-19 data sources. Addressing the impact of factors such as age distribution, vaccination, and emerging variants on the IFR time series is a pivotal aspect of our analysis. We expect our study to enhance our understanding of the genuine implications of the COVID-19 pandemic, subsequently benefiting mitigation strategies.more » « lessFree, publicly-accessible full text available May 1, 2025
-
Free, publicly-accessible full text available June 1, 2025
-
In this paper, we propose a new framework to detect adversarial examples motivated by the observations that random components can improve the smoothness of predictors and make it easier to simulate the output distribution of a deep neural network. With these observations, we propose a novel Bayesian adversarial example detector, short for BATER, to improve the performance of adversarial example detection. Specifically, we study the distributional difference of hidden layer output between natural and adversarial examples, and propose to use the randomness of the Bayesian neural network to simulate hidden layer output distribution and leverage the distribution dispersion to detect adversarial examples. The advantage of a Bayesian neural network is that the output is stochastic while a deep neural network without random components does not have such characteristics. Empirical results on several benchmark datasets against popular attacks show that the proposed BATER outperforms the state-of-the-art detectors in adversarial example detection.more » « less
-
High intratumoral heterogeneity is thought to be a poor prognostic indicator. However, the source of heterogeneity may also be important, as genomic heterogeneity is not always reflected in histologic or ‘visual’ heterogeneity. We aimed to develop a predictor of histologic heterogeneity and evaluate its association with outcomes and molecular heterogeneity. We used VGG16 to train an image classifier to identify unique, patient-specific visual features in 1655 breast tumors (5907 core images) from the Carolina Breast Cancer Study (CBCS). Extracted features for images, as well as the epithelial and stromal image components, were hierarchically clustered, and visual heterogeneity was defined as a greater distance between images from the same patient. We assessed the association between visual heterogeneity, clinical features, and DNA-based molecular heterogeneity using generalized linear models, and we used Cox models to estimate the association between visual heterogeneity and tumor recurrence. Basal-like and ER-negative tumors were more likely to have low visual heterogeneity, as were the tumors from younger and Black women. Less heterogeneous tumors had a higher risk of recurrence (hazard ratio = 1.62, 95% confidence interval = 1.22–2.16), and were more likely to come from patients whose tumors were comprised of only one subclone or had a TP53 mutation. Associations were similar regardless of whether the image was based on stroma, epithelium, or both. Histologic heterogeneity adds complementary information to commonly used molecular indicators, with low heterogeneity predicting worse outcomes. Future work integrating multiple sources of heterogeneity may provide a more comprehensive understanding of tumor progression.more » « lessFree, publicly-accessible full text available July 1, 2025
-
more » « less
Abstract Background Estimating malaria risk associated with work locations and travel across a region provides local health officials with information useful to mitigate possible transmission paths of malaria as well as understand the risk of exposure for local populations. This study investigates malaria exposure risk by analysing the spatial pattern of malaria cases (primarily
Plasmodium vivax) in Ubon Ratchathani and Sisaket provinces of Thailand, using an ecological niche model and machine learning to estimate the species distribution ofP. vivax malaria and compare the resulting niche areas with occupation type, work locations, and work-related travel routes.Methods A maximum entropy model was trained to estimate the distribution of
P. vivax malaria for a period between January 2019 and April 2020, capturing estimated malaria occurrence for these provinces. A random simulation workflow was developed to make region-based case data usable for the machine learning approach. This workflow was used to generate a probability surface for the ecological niche regions. The resulting niche regions were analysed by occupation type, home and work locations, and work-related travel routes to determine the relationship between these variables and malaria occurrence. A one-way analysis of variance (ANOVA) test was used to understand the relationship between predicted malaria occurrence and occupation type.Results The MaxEnt (full name) model indicated a higher occurrence of
P. vivax malaria in forested areas especially along the Thailand–Cambodia border. The ANOVA results showed a statistically significant difference between average malaria risk values predicted from the ecological niche model for rubber plantation workers and farmers, the two main occupation groups in the study. The rubber plantation workers were found to be at higher risk of exposure to malaria than farmers in Ubon Ratchathani and Sisaket provinces of Thailand.Conclusion The results from this study point to occupation-related factors such as work location and the routes travelled to work, being risk factors in malaria occurrence and possible contributors to transmission among local populations.
