bluuebunny/crossref_metadata_2025_split huggingface dataset:
Distance spectacle‐wearing habits in older patients in England
Authors: Hughes Amy R. , Elliott David B. 
Published: June 2023

AbstractPurposeTo report the proportion of older people in England who wear distance spectacles full time, part time and rarely, and to investigate factors that influence how much the distance vision (DV) correction is worn.MethodsA two‐part questionnaire investigating the spectacle‐wearing habits of older people was developed and completed by 322 participants (age 72 years ±7.7, range 60–94). A subcohort of 209 DV correction wearers with a mean spherical equivalent (MSE) of <±4.00DS was selected for a logistic regression to investigate which factors influence how much the DV correction is used.ResultsIn total, 43% of emmetropic, and 55% of pseudophakic, DV spectacle wearers wear their correction full time. Lens type, MSE and the age that participants first wore a DV correction significantly predicted DV correction wearing habit (adjusted R2 = 0.36), with lens type being the strongest predicting factor and progressive users wearing their spectacles 37% more than those using single vision lenses.ConclusionsMany patients appear to consider convenience more important than being spectacle independent at distance, with lens type the most significant influencing factor of how much those with low/moderate refractive error wear their distance correction. Many emmetropes and pseudophakes choose to wear their progressive or bifocal spectacles full time, and the emmetropia provided by cataract surgery does not provide independence from full‐time spectacle wear for many patients. The optometrist has a key role in discussing both choice of spectacle lens correction and the refractive outcome options of cataract surgery with patients.
Locating religion in contemporary art
Authors: Arya Rina 
Published: June 2023

AbstractThe place of religion in the context of contemporary art is fraught and complex. This article discusses three prominent ways in which religion is explored in contemporary art: in sociopolitics, in art that transgresses, and in the creation of spaces of contemplation, some of which may be ‘religious’. Each of these ways have in common the exploration of religion primarily in terms of its lived experience and practices (within identity and the material world) rather than through religious belief or the institutions of religion.
Rice‐farming areas report more anxiety across two years of the COVID‐19 pandemic in China
Authors: Zhang Xinyi , English Alexander , Talhelm Thomas , Nam Benjamin H. , Wei Liuqing 
Published: June 2023

AbstractCultures responded to the COVID‐19 pandemic differently. We investigated cultural differences in mental health during the pandemic. We found regional differences in people's reports of anxiety in China over two years from 2020 to 2021 (N = 1186). People in areas with a history of rice farming reported more anxiety than people in wheat‐farming areas. Next, we explored more proximal mechanisms that could help link the distal, historical factor of rice farming to people's modern experience of anxiety. Rice areas scored higher on collectivism and tight social norms than wheat areas, and collectivism, rather than norm tightness, mediated the rice‐anxiety relationship. These findings advance our understanding of the distal sources of cultural differences, the proximal mechanisms, and mental health problems during the pandemics.
Repeated High-Intensity Technique Training and Repeated Sprint Training Elicit Similar Adjustment in Physiological Responses But Divergent Perceptual Responses and Combat-Related Performances in Adolescent Taekwondo Matches
Authors: Ouergui Ibrahim , Delleli Slaheddine , Messaoudi Hamdi , Bridge Craig Alan , Chtourou Hamdi , Franchini Emerson , Ardigò Luca Paolo 
Published: June 2023

Purpose: This study investigated the effects of 4 weeks of repeated sprint training (RST) versus repeated high-intensity technique training (RTT) on the physiological responses (ie, blood lactate), mean and peak heart rate, rating of perceived exertion, technical–tactical performance, and time–motion variables during simulated taekwondo combats. Methods: Twenty-four taekwondo athletes (18 male and 6 female; age: 16 [1] y) were randomly and equally assigned to RST (10 × 35-m running sprints interspersed by 10-s rest) or RTT (10 × 6-s bandal-tchagui kicking executions interspersed by 10-s rest) groups in addition to their regular training. Both groups performed simulated combats before and after training. Results: Delta lactate and peak heart rate were attenuated following training (P < .001 and P = .03, respectively), with no differences identified between RTT and RST conditions. Rating of perceived exertion decreased after training only in the RTT (P = .002). Time fighting and preparatory activities increased following training (P < .001), with higher values observed following RTT than RST (P < .001). Nonpreparatory time decreased after training (P < .001), with more pronounced reductions observed following RTT when compared to RST (P < .001). The number of single attacks decreased only following RST (P < .001), whereas combined attacks increased only after RTT training (P < .001). Conclusions: Similar adjustments in the physiological responses to combat were observed following 4 weeks of either RST or RTT, but RTT elicited more favorable perceptual responses and combat-related performance. This highlights the importance of specificity of training and its effective transfer to combat.
Southwest Borneo, an autochthonous Pangea-Eurasia assembly proxy: Insights from detrital zircon record
Authors: Quek Long Xiang , Li Shan , Morley Christopher K. , Ghani Azman A. , Zhu Junbin , Roselee Muhammad Hatta , Murthadha Sayed , Rahmat Rezal , Lai Yu-Ming , Lintjewas Lediyantje 
Published: June 2023

Abstract
The current tectonic model for Borneo in SE Asia suggests that the SW Borneo block rifted from NW Australia at ca. 190 Ma and drifted across the Tethyan Ocean to collide with Eurasia in the Early Cretaceous. But, the global zircon Hf trend after 200 Ma indicates that circum-Pacific-style accretionary orogens prevail. The SW Borneo detrital zircon data set, which combines our new data with previous data, shows consistent age peaks (ca. 250 Ma, 1.9–1.8 Ga, and 2.5–2.4 Ga) in late Permian to Early Cretaceous samples. The Banda terranes, a notable block derived from NW Australia, have distinct detrital zircon age peaks for pre-breakup and post-breakup. Available Borneo detrital zircon εHf(t) values for ca. 1.8 Ga and 2.4 Ga are indistinguishable from those of NW Australia sources, but εHf(t) values for 300–200 Ma are more negative than those from the Gondwanide orogen and are more similar to those from the Peninsular Malaysia Indosinian orogen. We suggest SW Borneo is a Triassic accretion zone at eastern Cimmeria that rifted from NW Australia in the Permian. The ca. 250 Ma negative εHf(t) values present in samples are characteristic of Tethyan-style collisional orogens and show participation in Pangea assembly. SW Borneo underwent further autochthonous accretion along its SE margin (ca. 186 Ma and ca. 140 Ma) in a Jurassic Meso-Tethys and Paleo-Pacific supra–subduction zone setting. Our revision locates SW Borneo with other SE Tethysides blocks in Eurasia where accretionary orogens have influenced rises after 200 Ma.
Jordan Property for the Cremona Group over a Finite Field
Authors: Prokhorov Yuri G. , Shramov Constantin A. 
Published: June 2023

Abstract
We show that the Cremona group of rank $$2$$ over a finite field is Jordan, and provide an upper bound for its Jordan constant which is sharp when the number of elements in the field is different from $$2$$, $$4$$, and $$8$$.
Coincident $$f(\mathbb {Q})$$ gravity: black holes, regular black holes, and black bounces
Authors: Junior José Tarciso S. S. , Rodrigues Manuel E. 
Published: June 2023

AbstractIn this paper, we will use the coincident gauge to investigate new solutions of the$$f(\mathbb {Q})$$f(Q)theory applied in the context of black holes, regular black holes, and the black-bounce spacetime. For each of these approaches, we compute the linear solutions and the solutions with the constraint that the non-metricity scalar is zero. We also analyze the geodesics of each solution to interpret whether the spacetime is extensible or not, find the Kretschmann scalar to determine the regularity along spacetime, and in the context of regular black holes and black-bounce, we calculate the energy conditions. In the latter black-bounce case we realize that the null energy condition (NEC), specifically the$$NEC_1=WEC_1=SEC_1\leftrightarrow \rho +p_{r}\ge 0$$NEC1=WEC1=SEC1↔ρ+pr≥0, is satisfied outside the event horizon.
ON MODIFIED VARIANTS OF CLASSICAL TROJAN Y CHROMOSOME MODEL WITH GLOBAL SOLUTIONS
Authors: TAKYI ERIC M. , BEAUREGARD MATTHEW A. , PARSHAD RANA D. 
Published: June 2023

The Trojan Y Chromosome (TYC) strategy is a biological control method for controlling invasive populations with an XX–XY sex determinism, wherein a modified organism is introduced into an invasive population to skew the sex ratio over time, causing local extinction. However, the classical three compartment TYC model possesses blow-up solutions, for large initial conditions [Takyi EM, Beauregard MA, Griffin T, Bobo L, Parshad RD, On large and small data blow-up solutions in the Trojan Y Chromosome model, Axioms 11(3):120, 2022]. We investigate model improvements via accounting for a modified logistic term, female mating preference, competition between males and supermales and pair formation. Each one of these models is dynamically explored and is shown to possess global in-time non-negative solutions, in any parameter and initial data regime, and the models are also effective in facilitating extinction of the invasive wild type.
Modular Control Plane Verification via Temporal Invariants
Authors: Alberdingk Thijm Timothy , Beckett Ryan , Gupta Aarti , Walker David 
Published: June 2023

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine.
Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.
Garbage-Collection Safety for Region-Based Type-Polymorphic Programs
Authors: Elsman Martin 
Published: June 2023

Region inference offers a mechanism to reduce (and sometimes entirely remove) the need for reference-tracing garbage collection by inferring where to insert allocation and deallocation instructions in a program at compile time. When the mechanism is combined with techniques for reference-tracing garbage collection, which is helpful in general to support programs with very dynamic memory behaviours, it turns out that region-inference is complementary to adding generations to a reference-tracing collector. However, region-inference and the associated region-representation analyses that make such a memory management strategy perform well in practice are complex, both from a theoretical point-of-view and from an implementation point-of-view.In this paper, we demonstrate a soundness problem with existing theoretical developments, which have to do with ensuring that, even for higher-order polymorphic programs, no dangling-pointers appear during a reference-tracing collection. This problem has materialised as a practical soundness problem in a real implementation based on region inference. As a solution, we present a modified, yet simple, region type-system that captures garbage-collection effects, even for polymorphic higher-order code, and outline how region inference and region-representation analyses are adapted to the new type system. The new type system allows for associating simpler region type-schemes with functions, compared to original work, makes it possible to combine region-based memory management with partly tag-free reference-tracing (and generational) garbage-collection, and repairs previously derived work that is based on the erroneous published results.
Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation
Authors: Mangipudi Shamiek , Chuprikov Pavel , Eugster Patrick , Viering Malte , Savvides Savvas 
Published: June 2023

As more organizations are leveraging third-party cloud and edge data centers to process data efficiently, the issue of preserving data confidentiality becomes increasingly important. In response, numerous security mechanisms have been introduced and promoted in recent years including software-based ones such as homomorphic encryption, as well as hardware-based ones such as Intel SGX and AMD SEV. However these mechanisms vary in their security properties, performance characteristics, availability, and application modalities, making it hard for programmers to judiciously choose and correctly employ the right one for a given data query.This paper presents a mechanism-independent approach to distributed confidentiality-preserving data analytics. Our approach hinges on a core programming language which abstracts the intricacies of individual security mechanisms. Data is labeled using custom confidentiality levels arranged along a lattice in order to capture its exact confidentiality constraints. High-level mappings between available mechanisms and these labels are captured through a novel expressive form of security policy. Confidentiality is guaranteed through a type system based on a novel formulation of noninterference, generalized to support our security policy definition. Queries written in a largely security-agnostic subset of our language are transformed to the full language to automatically use mechanisms in an efficient, possibly combined manner, while provably preserving confidentiality in data queries end-to-end. We prototype our approach as an extension to the popular Apache Spark analytics engine, demonstrating the significant versatility and performance benefits of our approach over single hardwired mechanisms --- including in existing systems --- without compromising on confidentiality.
Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis
Authors: Ma Wenjie , Yang Shengyuan , Tan Tian , Ma Xiaoxing , Xu Chang , Li Yue 
Published: June 2023

Over the past decades, context sensitivity has been considered as one of the most effective ideas for improving the precision of pointer analysis for Java. Different from the extremely fast context-insensitivity approach, context sensitivity requires every program method to be analyzed under different contexts for separating the static abstractions of different dynamic instantiations of the method’s variables and heap objects, and thus reducing spurious object flows introduced by method calls. However, despite great precision benefits, as each method is equivalently cloned and analyzed under each context, context sensitivity brings heavy efficiency costs. Recently, numerous selective context-sensitive approaches have been put forth for scaling pointer analysis to large and complex Java programs by applying contexts only to the selected methods while analyzing the remaining ones context-insensitively; however, because the selective approaches do not fundamentally alter the primary methodology of context sensitivity (and do not thus remove its efficiency bottleneck), they produce much improved but still limited results.
In this work, we present a fundamentally different approach called Cut-Shortcut for fast and precise pointer analysis for Java. Its insight is simple: the main effect of cloning methods under different contexts is to filter spurious object flows that have been merged inside a callee method; from the view of a typical pointer flow graph (PFG), such effect can be simulated by cutting off (Cut) the edges that introduce precision loss to certain pointers and adding Shortcut edges directly from source pointers to the target ones circumventing the method on PFG. As a result, we can achieve the effect of context sensitivity without contexts. We identify three general program patterns and develop algorithms based on them to safely cut off and add shortcut edges on PFG, formalize them and formally prove the soundness. To comprehensively validate Cut-Shortcut’s effectiveness, we implement two versions of Cut-Shortcut for two state-of-the-art pointer analysis frameworks for Java, one in Datalog for the declarative Doop and the other in Java for the imperative Tai-e, and we consider all the large and complex programs used in recent literatures that meet the experimental requirements. The evaluation results are extremely promising: Cut-Shortcut is even able to run faster than context insensitivity for most evaluated programs while obtaining high precision that is comparable to context sensitivity (if scalable) in both frameworks. This is for the first time that we have been able to achieve such a good efficiency and precision trade-off for those hard-to-analyze programs, and we hope Cut-Shortcut could offer new perspectives for developing more effective pointer analysis for Java in the future.
Responsive Parallelism with Synchronization
Authors: Muller Stefan K. , Singer Kyle , Keeney Devyn Terra , Neth Andrew , Agrawal Kunal , Lee I-Ting Angelina , Acar Umut A. 
Published: June 2023

Many concurrent programs assign priorities to threads to improve responsiveness. When used in conjunction with synchronization mechanisms such as mutexes and condition variables, however, priorities can lead to priority inversions, in which high-priority threads are delayed by low-priority ones. Priority inversions in the use of mutexes are easily handled using dynamic techniques such as priority inheritance, but priority inversions in the use of condition variables are not well-studied and dynamic techniques are not suitable.
In this work, we use a combination of static and dynamic techniques to prevent priority inversion in code that uses mutexes and condition variables. A type system ensures that condition variables are used safely, even while dynamic techniques change thread priorities at runtime to eliminate priority inversions in the use of mutexes. We prove the soundness of our system, using a model of priority inversions based on cost models for parallel programs. To show that the type system is practical to implement, we encode it within the type systems of Rust and C++, and show that the restrictions are not overly burdensome by writing sizeable case studies using these encodings, including porting the Memcached object server to use our C++ implementation.
Cakes That Bake Cakes: Dynamic Computation in CakeML
Authors: Sewell Thomas , Myreen Magnus O. , Tan Yong Kiam , Kumar Ramana , Mihajlovic Alexander , Abrahamsson Oskar , Owens Scott 
Published: June 2023

We have extended the verified CakeML compiler with a new language primitive,
Eval, which permits evaluation of new CakeML syntax at runtime. This new
implementation supports an ambitious form of compilation at runtime and dynamic
execution, where the original and dynamically added code can share
(higher-order) values and recursively call each other. This is, to our
knowledge, the first verified run-time environment capable of supporting a
standard LCF-style theorem prover design.
Modifying the modern CakeML compiler pipeline and proofs to support
a dynamic computation semantics was an extensive project. We review the
design decisions, proof techniques, and proof engineering lessons
from the project, and highlight some unexpected complications.
Type-Checking CRDT Convergence
Authors: Zakhour George , Weisenburger Pascal , Salvaneschi Guido 
Published: June 2023

Conflict-Free Replicated Data Types (CRDTs) are a recent approach for keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. For correct operation, CRDTs rely on a merge function that is commutative, associative and idempotent. Ensuring that such algebraic properties are satisfied by implementations, however, is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of a model, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.
In this paper, we present Propel, a programming language with a type system that captures the algebraic properties required by a correct CRDT implementation. The Propel type system deduces such properties by case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction for free. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties. We provide an implementation of Propel as a Scala embedding, we implement several CRDTs, verify them with Propel and compare the verification process with four state-of-the-art verification tools. Our evaluation shows that Propel is able to automatically deduce the properties that are relevant for common CRDT implementations found in open-source libraries even in cases in which competitors timeout.
Efficient Parallel Functional Programming with Effects
Authors: Arora Jatin , Westrick Sam , Acar Umut A. 
Published: June 2023

Although functional programming languages simplify writing safe parallel programs by helping programmers to avoid data races, they have traditionally delivered poor performance. Recent work improved performance by using a hierarchical memory architecture that allows processors to allocate and reclaim memory independently without any synchronization, solving thus the key performance challenge afflicting functional programs. The approach, however, restricts mutation, or memory effects, so as to ensure "disentanglement", a low-level memory property that guarantees independence between different heaps in the hierarchy.This paper proposes techniques for supporting entanglement and for allowing functional programs to use mutation at will. Our techniques manage entanglement by distinguishing between disentangled and entangled objects and shielding disentangled objects from the cost of entanglement management. We present a semantics that formalizes entanglement as a property at the granularity of memory objects, and define several cost metrics to reason about and bound the time and space cost of entanglement. We present an implementation of the techniques by extending the MPL compiler for Parallel ML. The extended compiler supports all features of the Parallel ML language, including unrestricted effects. Our experiments using a variety of benchmarks show that MPL incurs a small time and space overhead compared to sequential runs, scales well, and is competitive with languages such as C++, Go, Java, OCaml. These results show that our techniques can marry the safety benefits of functional programming with performance.