bluuebunny/crossref_metadata_2025 huggingface dataset:
PureCake: A Verified Compiler for a Lazy Functional Language
Authors: Kanabar Hrutvik , Vivien Samuel , Abrahamsson Oskar , Myreen Magnus O. , Norrish Michael , Pohjola Johannes Åman , Zanetti Riccardo
Published: June 2023

We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.
Taype: A Policy-Agnostic Language for Oblivious Computation
Authors: Ye Qianchuan , Delaware Benjamin
Published: June 2023

Secure multiparty computation (MPC) allows for joint computation over private data from multiple entities, usually backed by powerful cryptographic techniques that protect sensitive data. Several high-level programming languages have been proposed to make writing MPC applications accessible to non-experts. These languages typically require developers to enforce security policies within the logic of the secure application itself, making it difficult to update security requirements, or to experiment with different policies. This paper presents the design and implementation of Taype, a language that permits security concerns to be decoupled from the program logic. To do so, Taype provides the first implementation of oblivious algebraic data types and tape semantics, two language features recently proposed by a core calculus for oblivious computation, λ

OADT
+

. We evaluate our implementation of Taype on a range of benchmarks, demonstrating its ability to encode a range of security polices for a rich class of data types.
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
Authors: Rao Xiaojia , Georges Aïna Linn , Legoupil Maxime , Watt Conrad , Pichon-Pharabod Jean , Gardner Philippa , Birkedal Lars
Published: June 2023

WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.
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.
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
Authors: Kuepper Joel , Erbsen Andres , Gross Jason , Conoly Owen , Sun Chuyue , Tian Samuel , Wu David , Chlipala Adam , Chuengsatiansup Chitchanok , Genkin Daniel , Wagner Markus , Yarom Yuval
Published: June 2023

Most software domains rely on compilers to translate high-level code to multiple different machine languages,
with performance not too much worse than what developers would have the patience to write directly
in assembly language. However, cryptography has been an exception, where many performance-critical
routines have been written directly in assembly (sometimes through metaprogramming layers). Some past
work has shown how to do formal verification of that assembly, and other work has shown how to generate
C code automatically along with formal proof, but with consequent performance penalties vs. the best-
known assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic
functional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized
proof (in Coq) whose final theorem statement mentions little beyond the input functional program and the
operational semantics of x86-64 assembly. On the optimization side, we apply randomized search through the
space of assembly programs, with repeated automatic benchmarking on target CPUs. On the formal-verification
side, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR
code) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset
of known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical,
e.g. producing new fastest-known implementations of finite-field arithmetic for both Curve25519 (part of the
TLS standard) and the Bitcoin elliptic curve secp256k1 for the Intel 12𝑡ℎ and 13𝑡ℎ generations.
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.
Obtaining Information Leakage Bounds via Approximate Model Counting
Authors: Saha Seemanta , Ghentiyala Surendra , Lu Shihua , Bang Lucas , Bultan Tevfik
Published: June 2023

Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.
Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
Authors: Pailoor Shankara , Chen Yanju , Wang Franklyn , Rodríguez Clara , Van Geffen Jacob , Morton Jason , Chu Michael , Gu Brian , Feng Yu , Dillig Işıl
Published: June 2023

As zero-knowledge proofs gain increasing adoption, the cryptography community has designed domain-specific languages (DSLs) that facilitate the construction of zero-knowledge proofs (ZKPs). Many of these DSLs, such as Circom, facilitate the construction of arithmetic circuits, which are essentially polynomial equations over a finite field. In particular, given a program in a zero-knowledge proof DSL, the compiler automatically produces the corresponding arithmetic circuit. However, a common and serious problem is that the generated circuit may be underconstrained, either due to a bug in the program or a bug in the compiler itself. Underconstrained circuits admit multiple witnesses for a given input, so a malicious party can generate bogus witnesses, thereby causing the verifier to accept a proof that it should not. Because of the increasing prevalence of such arithmetic circuits in blockchain applications, several million dollars worth of cryptocurrency have been stolen due to underconstrained arithmetic circuits.

Motivated by this problem, we propose a new technique for finding ZKP bugs caused by underconstrained polynomial equations over finite fields. Our method performs semantic reasoning over the finite field equations generated by the compiler to prove whether or not each signal is uniquely determined by the input. Our proposed approach combines SMT solving with lightweight uniqueness inference to effectively reason about underconstrained circuits. We have implemented our proposed approach in a tool called
QED

2

and evaluate it on 163 Circom circuits. Our evaluation shows that
QED

2

can successfully solve 70% of these benchmarks, meaning that it either verifies the uniqueness of the output signals or finds a pair of witnesses that demonstrate non-uniqueness of the circuit. Furthermore,
QED

2

has found 8 previously unknown vulnerabilities in widely-used circuits.
Flux: Liquid Types for Rust
Authors: Lehmann Nico , Geller Adam T. , Vazou Niki , Jhala Ranjit
Published: June 2023

We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the Stacked Borrows aliasing model to prove that "well-borrowed evaluations of well-typed programs do not get stuck". Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations-including complex quantified invariants describing the contents of containers-via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid typing makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 14%), to nothing at all.
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.
Absynthe: Abstract Interpretation-Guided Synthesis
Authors: Guria Sankha Narayan , Foster Jeffrey S. , Van Horn David
Published: June 2023

Synthesis tools have seen significant success in recent times. However,
past approaches often require a complete and accurate embedding of the source
language in the logic of the underlying solver, an approach difficult for
industrial-grade languages. Other approaches couple the semantics of the source
language with purpose-built synthesizers, necessarily tying the synthesis engine
to a particular language model.
In this paper, we propose Absynthe, an alternative approach based on
user-defined abstract semantics that aims to be both lightweight and language
agnostic, yet effective in guiding the search for programs.
A synthesis goal in Absynthe is specified as an abstract
specification in a lightweight user-defined abstract domain and concrete test
cases.
The synthesis engine is parameterized by the abstract semantics and independent
of the source language.
Absynthe validates candidate programs against test cases using the
actual concrete language implementation to ensure correctness.
We formalize the synthesis rules for Absynthe
and describe how the key ideas are scaled-up in our implementation in Ruby. We
evaluated Absynthe on SyGuS strings benchmark and found it competitive with
other enumerative search solvers. Moreover, Absynthe's ability to combine
abstract domains allows the user to move along a cost spectrum, i.e., expressive
domains prune more programs but require more time. Finally, to verify
Absynthe can act as a general purpose synthesis tool, we use Absynthe to
synthesize Pandas data frame manipulating programs in Python using simple
abstractions like types and column labels of a data frame. Absynthe reaches
parity with AutoPandas, a deep learning based tool for the same benchmark
suite. In summary, our results demonstrate Absynthe is a
promising step forward towards a general-purpose approach to synthesis that may
broaden the applicability of synthesis to more full-featured languages.
Extensible Metatheory Mechanization via Family Polymorphism
Authors: Jin Ende , Amin Nada , Zhang Yizhou
Published: June 2023

With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This paper presents a novel language design geared towards extensible metatheory mechanization in a proof assistant. The new design achieves reuse and extensibility via a form of family polymorphism, an object-oriented idea, that allows code and proofs to be polymorphic to their enclosing families. Our development addresses technical challenges that arise from the underlying language of a proof assistant being simultaneously functional, dependently typed, a logic, and an interactive tool. Our results include (1) a prototypical implementation of the language design as a Coq plugin, (2) a dependent type theory capturing the essence of the language mechanism and its consistency and canonicity results, and (3) case studies showing how the new expressiveness naturally addresses real programming challenges in metatheory mechanization.
Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs
Authors: Lecoeur Bastien , Mohsin Hasan , Donaldson Alastair F.
Published: June 2023

We introduce program reconditioning, a method for allowing program generation and differential testing to be used to find miscompilation bugs, and test-case reduction to be used to simplify bug-triggering programs, even when (a) the programming language of interest features undefined behaviour (UB) and (b) no tools exist to detect and avoid this UB. We present two program generation tools based on our reconditioning idea: GLSLsmith for the OpenGL Shading Language (GLSL), a widely-used language for graphics programming, and WGSLsmith for the WebGPU Shading Language (WGSL), a new language for web-based graphics rendering. GLSL features many UBs, but unlike for languages such as C and C++ no tools exist to detect them automatically. While the WGSL language specification features very limited UB, early WGSL implementations do exhibit UB, for reasons of initial implementation simplicity, making it challenging to test them to quickly detect and eliminate unrelated miscompilation bugs. Thanks to reconditioning, we show that GLSLsmith and WGSLsmith allow differential testing and test-case reduction to be applied to compilers for GLSL and WGSL for the first time, despite the unavailability of UB detection techniques for these languages. Through a large testing campaign, we have found 24 and 33 bugs in GLSL and WGSL compilers, respectively. We present experiments showing that when reconditioning is disabled, compiler testing leads to a high rate of test programs that appear to trigger miscompilation bugs, but actually just feature UB. We also present a novel approach to managing floating-point roundoff error using reconditioning, implemented for both GLSL and WGSL.
Prompting Is Programming: A Query Language for Large Language Models
Authors: Beurer-Kellner Luca , Fischer Marc , Vechev Martin
Published: June 2023

Large language models have demonstrated outstanding performance on a wide range of tasks such as question answering and code generation. On a high level, given an input, a language model can be used to automatically complete the sequence in a statistically-likely way. Based on this, users prompt these models with language instructions or examples, to implement a variety of downstream tasks. Advanced prompting methods can even imply interaction between the language model, a user, and external tools such as calculators. However, to obtain state-of-the-art performance or adapt language models for specific tasks, complex task- and model-specific programs have to be implemented, which may still require ad-hoc interaction.

Based on this, we present the novel idea of Language Model Programming (LMP). LMP generalizes language model prompting from pure text prompts to an intuitive combination of text prompting and scripting. Additionally, LMP allows constraints to be specified over the language model output. This enables easy adaption to many tasks while abstracting language model internals and providing high-level semantics.

To enable LMP, we implement LMQL (short for Language Model Query Language), which leverages the constraints and control flow from an LMP prompt to generate an efficient inference procedure that minimizes the number of expensive calls to the underlying language model.

We show that LMQL can capture a wide range of state-of-the-art prompting methods in an intuitive way, especially facilitating interactive flows that are challenging to implement with existing high-level APIs. Our evaluation shows that we retain or increase the accuracy on several downstream tasks, while also significantly reducing the required amount of computation or cost in the case of pay-to-use APIs (26-85% cost savings).
Register Tiling for Unstructured Sparsity in Neural Network Inference
Authors: Wilkinson Lucas , Cheshmi Kazem , Dehnavi Maryam Mehri
Published: June 2023

Unstructured sparse neural networks are an important class of machine learning (ML) models, as they compact model size and reduce floating point operations. The execution time of these models is frequently dominated by the sparse matrix multiplication (SpMM) kernel,
C
=
A
×
B
, where
A
is a sparse matrix, and
B
and
C
are dense matrices. The unstructured sparsity pattern of matrices in pruned machine learning models along with their sparsity ratio has rendered useless the large class of libraries and systems that optimize sparse matrix multiplications. Reusing registers is particularly difficult because accesses to memory locations should be known statically. This paper proposes Sparse Register Tiling, a new technique composed of an unroll-and-sparse-jam transformation followed by data compression that is specifically tailored to sparsity patterns in ML matrices. Unroll-and-sparse-jam uses sparsity information to jam the code while improving register reuse. Sparse register tiling is evaluated across 2396 weight matrices from transformer and convolutional models with a sparsity range of 60-95% and provides an average speedup of 1.72× and 2.65× over MKL SpMM and dense matrix multiplication, respectively, on a multicore CPU processor. It also provides an end-to-end speedup of 2.12× for MobileNetV1 with 70% sparsity on an ARM processor commonly used in edge devices.
Sensor-Based Locomotion Data Mining for Supporting the Diagnosis of Neurodegenerative Disorders: A Survey
Authors: Zolfaghari Samaneh , Suravee Sumaiya , Riboni Daniele , Yordanova Kristina
Published: June 2023

Locomotion characteristics and movement patterns are reliable indicators of neurodegenerative diseases (NDDs). This survey provides a systematic literature review of locomotion data mining systems for supporting NDD diagnosis. We discuss techniques for discovering low-level locomotion indicators, sensor data acquisition and processing methods, and NDD detection algorithms. The survey presents a comprehensive discussion on the main challenges for this active area, including the addressed diseases, locomotion data types, duration of monitoring, employed algorithms, and experimental validation strategies. We also identify prominent open challenges and research directions regarding ethics and privacy issues, technological and usability aspects, and availability of public benchmarks.
Dynamic Power Management in Large Manycore Systems: A Learning-to-Search Framework
Authors: Narang Gaurav , Deshwal Aryan , Ayoub Raid , Kishinevsky Michael , Rao Doppa Janardhan , Pande Partha Pratim
Published: June 2023

The complexity of manycore System-on-chips (SoCs) is growing faster than our ability to manage them to reduce the overall energy consumption. Further, as SoC design moves toward three-dimensional (3D) architectures, the core's power density increases leading to unacceptable high peak chip temperatures. In this article, we consider the optimization problem of dynamic power management (DPM) in manycore SoCs for an allowable performance penalty (say, 5%) and admissible peak chip temperature. We employ a machine learning– (ML) based DPM policy, which selects the voltage/frequency levels for different cluster of cores as a function of the application workload features such as core computation and inter-core traffic, and so on. We propose a novel learning-to-search (L2S) framework to automatically identify an optimized sequence of DPM decisions from a large combinatorial space for joint energy-thermal optimization for one or more given applications. The optimized DPM decisions are given to a supervised learning algorithm to train a DPM policy, which mimics the corresponding decision-making behavior. Our experiments on two different manycore architectures designed using wireless interconnect and monolithic 3D demonstrate that principles behind the L2S framework are applicable for more than one configuration. Moreover, L2S-based DPM policies achieve up to 30% energy-delay product savings and reduce the peak chip temperature by up to 17 °C compared to the state-of-the-art ML methods for an allowable performance overhead of only 5%.
Enhanced Ozone Aging Resistance of Natural Rubber with 2-Mercaptobenzothiazole as the Constant-Viscosity Agent
Authors: Zhou Juan , Deng Peng , Gui Hongxing , Xu Junxiao , Liao Jianhe , Ding Aiwu
Published: June 2023

For the actual storage and serving, a phenomenon of hardening and cracking always occurs in the natural rubber (NR), which sharply reduces the mechanical performance and hinders the further application of NR. Recently, some type of constant-viscosity agent has played a key role to be used for the treatment of NR, especially for the effect of ozone aging resistance. In this study, 2-mercaptobenzothiazole (MBT) was introduced into NR, and the constant viscosity and ozone aging resistance of NR with different contents of MBT were investigated using an accelerated storage experiment and an ozone aging experiment, respectively. The results indicated that the addition of MBT could improve the constant viscosity of NR in a certain degree. With the MBT content of 0.15%, NR/MBT-0.15 obtained a best ozone aging resistance and maintained the original high tensile strength. Therefore, it provided a promising route to design and prepare NR with high-quality ozone aging resistance.
Convoluted Meander Line-Inspired Metallic Surface Filter for Bluetooth and WLAN Bands
Authors: Bagwari Ashish , Jindal Payal , Yadav Ajay , Tiwari Rahul , Sharma Sudhir Kumar , Logeshwaran J.
Published: June 2023

A convoluted meander line integrated cross dipole metallic structure with a dual-bandstop feature is presented in this manuscript. The investigated frequency-selective surface (FSS) exhibits the bandstopping characteristics for the Bluetooth (2.4 GHz) and WLAN (5.5 GHz) applications with a miniaturized unit cell size of 9.7 × 9.7 mm2. The proposed design has a polarization insensitivity feature for the TE and TM polarized waves’ incidents at 0°–60° with an interval of 15° angle. The equivalent circuit model of the presented FSS unit cell is also discussed and their limped element values are presented. The FSS design has a compact size which makes it favorable for low-profile band-filtering systems and multipath EM wave’s insensitivity. The suggested FSS configuration has good correspondence with modelled and measured results.
Serotonin Syndrome with Monotherapy of Low-Dose Sertraline in an Adult Patient with Autism Spectrum Disorder
Authors: Madan Rohit , Platto Jody , Manoharan Senthil Rajaram , Monga Varun
Published: June 2023

Serotonin syndrome, also known as serotonin toxicity, is associated with increased serotonergic activity in the central and the peripheral nervous system. The symptoms can range from mild to potentially life threatening. Given the widespread use of serotonergic agents, the number of cases is on the rise. It is seen with therapeutic medication use, inadvertent interactions between drugs, and intentional self-poisoning, but still known cases with monotherapy of selective serotonin reuptake inhibitors are uncommon. Another known fact is that elevated whole blood serotonin, or hyperserotonemia, is one of the first biomarkers identified in autism spectrum disorder and is present in more than 25% of affected children. We present a case of a 32-year-old male with a history of autism spectrum disorder and depressive disorder who presented to the emergency department with restless agitation, neuromuscular excitability, and autonomic instability. He had been prescribed sertraline 50 mg which he had taken daily as prescribed for 4 days. On the fourth day, he presented to the emergency department with diffuse muscle stiffness, upper extremity tremors, ocular clonus, and inducible ankle clonus. He was diagnosed with probable serotonin syndrome utilizing Hunter’s criteria. Patient’s symptoms resolved within 24 hours with intravenous fluids, lorazepam, and discontinuation of sertraline. This case highlights the importance of a high degree of clinical suspicion in patients even on monotherapy of selective serotonin reuptake inhibitors in therapeutic doses, especially in children and adults with autism spectrum disorder. Due to preexisting hyperserotonemia, they may be more susceptible to serotonin syndrome than the general population.
Treatment for Aging Skin with Multifrequency Radiofrequency
Authors: Baek Eun Joo , Oh Dong Yeol , Suh Suk Bae , Park Eun Joo , Kim Kwang Ho
Published: June 2023

Background. Radiofrequency treatment improves skin aging‐related concerns by promoting collagen production. However, studies of the efficacy of multifrequency radiofrequency (MFRF) are lacking. Objectives. This study aimed to analyze the efficacy of MFRF for patients with aging skin. Methods. Three MFRF treatment sessions were performed for patients with concerns about skin aging. During these sessions, MFRF was applied to the face (but not the forehead). Pores, wrinkles, subjective satisfaction, and side effects were evaluated at the first visit and 4 weeks after the last treatment. Additionally, histological and immunohistochemical evaluations of collagen, elastic fibers, and STRO‐1 were performed. Results. Wrinkles and the subjective satisfaction of patients were significantly improved (p = 0.034 and p = 0.001, respectively). However, there was no significant effect on the number of pores (p = 0.429). All side effects that occurred after treatment were tolerable and transient. Histological findings revealed thickening of collagen bundles and elastic fibers. Additionally, increases in collagen I, collagen III, and STRO‐1 levels were observed using immunohistochemistry. Conclusions. MFRF treatment uses less energy than the existing radiofrequency equipment and can be an effective clinicopathologic modality for facial rejuvenation.
Structural, Electronic, Elastic, Mechanical, and Opto-Electronic Properties for ZnAg2SnS4 and ZnAg2Sn0.93Fe0.07S4 Photocatalyst Effort on Wastewater Treatment through the First Principle Study
Authors: Islam Mohammad Jahidul , Sohag Md. Sabbir Hasan , Chakma Unesco , Kumer Ajoy , Alam Md. Monsur , Nazrul Islam Khan Mohammed
Published: June 2023

The stannite structured ZnAg2SnS4 was developed from its parent composition ZnAg2GeS4, which is considered to be an excellent photocatalytic material, as the demands for photocatalytic effect on organic and waste water treatment have been increasing around the globe. First and foremost, the geometry optimization was performed by density functional theory (DFT) of the generalized gradient approximation (GGA) with Perdew–Burke–Ernzerhof (PBE)-ballpark figured as the successful candidate for computational screening containing heavy metal complexes. The structural geometry parameters were determined along with the electronic band structure, density of state (DOS), partial density of state (PDOS), Mulliken charge population, elastic constant, and optical characteristics. When the Ge (ZnAg2GeS4) atom has been swapped out by a Sn (ZnAg2SnS4) atom, the changes in band gap is noticeable, which rises from 0.94 eV to 1.15 eV with the same geometry and surface area. But, after 7% Fe doping, it has decreased to 0.32 eV. The PDOS demonstrates that the production of hydrogen for photocatalytic influence on wastewater treatment is dependent on the Fe atom's ability to induce and boost the electron density in both the conduction band and the valence band. The study of the elastic constant and mechanical constant revealed that these crystals are extremely stable in any environment. The dielectric constant and optical absorptions illustrate the superior evidence for photocatalytic activity. To sum up, it could be said that after doping of Fe, the elastic constant and mechanical constant show all universal anisotropic index crystals and ZnAg2Sn0.93Fe0.07S4 can absorb a variety of UV radiation, which raises the possibility that it could function as a photocatalyst.
Table S4 from Resolving the Pathogenesis of Anaplastic Wilms Tumors through Spatial Mapping of Cancer Cell Evolution
Authors: Rastegar Bahar , Andersson Natalie , Petersson Alexandra , Karlsson Jenny , Chattopadhyay Subhayan , Valind Anders , Jansson Caroline , Durand Geoffroy , Romerius Patrik , Jirström Karin , Holmquist Mengelbier Linda , Gisselsson David
Published: June 2023

Supplementary Table 4. Segmental aberrations. All 20 Wilms tumor (WT) cases and their corresponding samples are listed. ‘Sample position’ refers to the individual sample and its position in a certain paraffin block (see Figure 1 for details.) For each genetic event the following information is given: the ploidy level (Ploidy), chromosome (chr), the genomic start and end positions, genetic events annotated as gain, loss, CNNI (copy neutral imbalance) or homozygous loss, the length of the aberration (bp), which chromosomal cytoband, the median log2 ratio, allelic composition and mutated cell fraction (MCF). IR= intermediate risk, BT= blastemal type, DA= diffuse anaplasia. Genomic positions accordning to hg19.
Table S1 from Resolving the Pathogenesis of Anaplastic Wilms Tumors through Spatial Mapping of Cancer Cell Evolution
Authors: Rastegar Bahar , Andersson Natalie , Petersson Alexandra , Karlsson Jenny , Chattopadhyay Subhayan , Valind Anders , Jansson Caroline , Durand Geoffroy , Romerius Patrik , Jirström Karin , Holmquist Mengelbier Linda , Gisselsson David
Published: June 2023

Supplementary Table 1. Overview of the study cohort and the clinical data. This table contains basic clinical information, including age, sex, whether tumors were uni- or bilateral, histology, stage, risk group, treatment to which the resection specimen analyzed was subjected to, the final outcome and the record of adverse events.
Data from Resolving the Pathogenesis of Anaplastic Wilms Tumors through Spatial Mapping of Cancer Cell Evolution
Authors: Rastegar Bahar , Andersson Natalie , Petersson Alexandra , Karlsson Jenny , Chattopadhyay Subhayan , Valind Anders , Jansson Caroline , Durand Geoffroy , Romerius Patrik , Jirström Karin , Holmquist Mengelbier Linda , Gisselsson David
Published: June 2023

AbstractPurpose:
While patients with intermediate-risk (IR) Wilms tumors now have an overall survival (OS) rate of almost 90%, those affected by high-stage tumors with diffuse anaplasia have an OS of only around 50%. We here identify key events in the pathogenesis of diffuse anaplasia by mapping cancer cell evolution over anatomic space in Wilms tumors.
Experimental Design:
We spatially mapped subclonal landscapes in a retrospective cohort of 20 Wilms tumors using high-resolution copy-number profiling and TP53 mutation analysis followed by clonal deconvolution and phylogenetic reconstruction. Tumor whole-mount sections (WMS) were utilized to characterize the distribution of subclones across anatomically distinct tumor compartments.
Results:
Compared with non-diffuse anaplasia Wilms tumors, tumors with diffuse anaplasia showed a significantly higher number of genetically distinct tumor cell subpopulations and more complex phylogenetic trees, including high levels of phylogenetic species richness, divergence, and irregularity. All regions with classical anaplasia showed TP53 alterations. TP53 mutations were frequently followed by saltatory evolution and parallel loss of the remaining wild-type (WT) allele in different regions. Morphologic features of anaplasia increased with copy-number aberration (CNA) burden and regressive features. Compartments demarcated by fibrous septae or necrosis/regression were frequently (73%) associated with the emergence of new clonal CNAs, although clonal sweeps were rare within these compartments.
Conclusions:
Wilms tumors with diffuse anaplasia display significantly more complex phylogenies compared with non-diffuse anaplasia Wilms tumors, including features of saltatory and parallel evolution. The subclonal landscape of individual tumors was constrained by anatomic compartments, which should be considered when sampling tissue for precision diagnostics.
Supplementary Data from Dual PI3K/mTOR Inhibition in Colorectal Cancers with APC and PIK3CA Mutations
Authors: Foley Tyler M , Payne Susan N. , Pasch Cheri A. , Yueh Alex E. , Van De Hey Dana R , Korkos Demetra P , Clipson Linda , Maher Molly E , Matkowskyj Kristina A. , Newton Michael A. , Deming Dustin A.
Published: June 2023

S1. AP spheroids were plated and allowed to mature for 48 hours. S2. To address the issue of potentially slower growth of the spheres with the largest initial sizes, a change-point analysis was performed. S3. AP mice were treated with control (A) or BEZ235 (B) for 14 days. S4. AP mice were treated with BEZ235 or control for 14 days. S5. AP spheroids were treated with NVP-BYL719, BEZ235, LY3023414, or control for 24 hours. S5. AP spheroids were treated with NVP-BYL719, BEZ235, LY3023414, or control for 24 hours. Supplementary Table S1. AP spheroids were treated with NVP-BYL719, GDC0941, BEZ235, LY3023414, or control for 48 hours. Supplemental Table S2. AP mice were treated with BEZ235, LY3023414 or control for 14 days.
Supplementary Figure 1 from A Mendelian Randomization Analysis of 55 Genetically Predicted Metabolic Traits with Breast Cancer Survival Outcomes in the Pathways Study
Authors: Fiorica Peter N. , Sheng Haiyang , Zhu Qianqian , Roh Janise M , Laurent Cecile A. , Ergas Isaac J , Delmerico Jennifer , Kwan Marilyn L , Kushi Lawrence H , Ambrosone Christine B , Yao Song
Published: June 2023

Dot plot of findings from analysis of 2,696 White individuals
Optimizing Precision Medicine for Breast Cancer Brain Metastases with Functional Drug Response Assessment
Authors: Morikawa Aki , Li Jinju , Ulintz Peter , Cheng Xu , Apfel Athena , Robinson Dan , Hopkins Alex , Kumar-Sinha Chandan , Wu Yi-Mi , Serhan Habib , Verbal Kait , Thomas Dafydd , Hayes Daniel F. , Chinnaiyan Arul M. , Baladandayuthapani Veerabhadran , Heth Jason , Soellner Matthew B. , Merajver Sofia D. , Merrill Nathan
Published: June 2023

The development of novel therapies for brain metastases is an unmet need. Brain metastases may have unique molecular features that could be explored as therapeutic targets. A better understanding of the drug sensitivity of live cells coupled to molecular analyses will lead to a rational prioritization of therapeutic candidates. We evaluated the molecular profiles of 12 breast cancer brain metastases (BCBM) and matched primary breast tumors to identify potential therapeutic targets. We established six novel patient-derived xenograft (PDX) from BCBM from patients undergoing clinically indicated surgical resection of BCBM and used the PDXs as a drug screening platform to interrogate potential molecular targets. Many of the alterations were conserved in brain metastases compared with the matched primary. We observed differential expressions in the immune-related and metabolism pathways. The PDXs from BCBM captured the potentially targetable molecular alterations in the source brain metastases tumor. The alterations in the PI3K pathway were the most predictive for drug efficacy in the PDXs. The PDXs were also treated with a panel of over 350 drugs and demonstrated high sensitivity to histone deacetylase and proteasome inhibitors. Our study revealed significant differences between the paired BCBM and primary breast tumors with the pathways involved in metabolisms and immune functions. While molecular targeted drug therapy based on genomic profiling of tumors is currently evaluated in clinical trials for patients with brain metastases, a functional precision medicine strategy may complement such an approach by expanding potential therapeutic options, even for BCBM without known targetable molecular alterations.

Significance:

Examining genomic alterations and differentially expressed pathways in brain metastases may inform future therapeutic strategies. This study supports genomically-guided therapy for BCBM and further investigation into incorporating real-time functional evaluation will increase confidence in efficacy estimations during drug development and predictive biomarker assessment for BCBM.
A Mendelian Randomization Analysis of 55 Genetically Predicted Metabolic Traits with Breast Cancer Survival Outcomes in the Pathways Study
Authors: Fiorica Peter N. , Sheng Haiyang , Zhu Qianqian , Roh Janise M. , Laurent Cecile A. , Ergas Isaac J. , Delmerico Jennifer , Kwan Marilyn L. , Kushi Lawrence H. , Ambrosone Christine B. , Yao Song
Published: June 2023

Previous studies suggest associations of metabolic syndromes with breast cancer prognosis, yet the evidence is mixed. In recent years, the maturation of genome-wide association study findings has led to the development of polygenic scores (PGS) for many common traits, making it feasible to use Mendelian randomization to examine associations between metabolic traits and breast cancer outcomes. In the Pathways Study of 3,902 patients and a median follow-up time of 10.5 years, we adapted a Mendelian randomization approach to calculate PGS for 55 metabolic traits and tested their associations with seven survival outcomes. Multivariable Cox proportional hazards models were used to derive HRs and 95% confidence intervals (CI) with adjustment for covariates. The highest tertile (T3) of PGS for cardiovascular disease was associated with shorter overall survival (HR = 1.34, 95% CI = 1.11–1.61) and second primary cancer–free survival (HR = 1.31, 95% CI = 1.12–1.53). PGS for hypertension (T3) was associated with shorter overall survival (HR = 1.20, 95% CI = 1.00–1.43), second primary cancer–free survival (HR = 1.24, 95% CI = 1.06–1.45), invasive disease-free survival (HR = 1.18, 95% CI = 1.01–1.38), and disease-free survival (HR = 1.21, 95% CI = 1.04–1.39). PGS for serum cystatin C levels (T3) was associated with longer disease-free survival (HR = 0.82, 95% CI = 0.71–0.95), breast event-free survival (HR = 0.74, 95% CI = 0.61–0.91), and breast cancer–specific survival (HR = 0.72, 95% CI = 0.54–0.95). The above associations were significant at a nominal P < 0.05 level but not after correcting for multiple testing (Bonferroni P < 0.0009). Our analyses revealed notable associations of PGS for cardiovascular disease, hypertension, and cystatin C levels with breast cancer survival outcomes. These findings implicate metabolic traits in breast cancer prognosis.

Significance:

To our knowledge, this is the largest study of PGS for metabolic traits with breast cancer prognosis. The findings revealed significant associations of PGS for cardiovascular disease, hypertension, and cystatin C levels with several breast cancer survival outcomes. These findings implicate an underappreciated role of metabolic traits in breast cancer prognosis that would warrant further exploration.
Progressive Central Artery Occlusion, Ophthalmic Artery Occlusion, and Hemispheric Intracranial Thrombosis after COVID-19 mRNA Vaccine Application: Case Report
Authors: Chen Jinghua , Peltzer Cadynce , Buchowicz Bryce , Dawson Slaney Elizabeth , Maleki Arash
Published: June 2023

Thromboembolic events as a result of COVID-19 mRNA vaccination are a rare, though life-threatening complication. In this case report, we describe a 40-year-old female patient who developed central retinal artery and ophthalmic artery occlusion progressing to intracranial thrombosis 3 weeks after vaccination with the Pfizer-BioNTech COVID-19 vaccine. Initially, she presented with progressive acute and painless unilateral vision loss in her left eye. Dilated fundoscopy of left eye showed macular whitening with sparing of the area of cilioretinal artery distribution. Labs revealed a normal erythrocyte sedimentation rate, C-reactive protein, and platelet count. Computerized tomography angiography of the head and neck showed an occlusion of the entire left cervical internal carotid artery and occlusion of the origin of the left external carotid artery. Despite treatment with heparin, her vision declined to no light perception. Ten days later, the patient presented with right peripheral vision loss and was found to have a new left posterior cerebral artery/posterior inferior cerebellar artery stroke. Seventeen days later, she presented to the hospital with nausea and vertigo and was found to have a subacute infarction in the left parietal lobe corresponding to left anterior communicating artery/middle cerebral artery watershed territory. Hypercoagulable disorders, vasculitis, cardiac arrhythmias, and intraventricular thrombi were excluded. Fundus fluorescein angiography confirmed central retinal artery occlusion and ophthalmic artery occlusion with impressive retina and choroid changes in fluorescein angiography patterns. This complication of mRNA COVID-19 vaccination has not been previously described in the literature and should be considered even weeks after initial presentation.
Moda afro-brasileira é design de resistência da luta negra no Brasil
Authors:   Universidade de São Paulo. Escola de Artes Ciências e Humanidades, Santos Maria do Carmo Paulino dos
Published: June 2023

Esta obra, intitulada Moda afro-brasileira é design de resistência na luta negra no Brasil, apresenta alguns textos sobre a moda feita por pessoas negras como linguagem de expressão no vestir e no design de joias, com um re-corte sobre a cultura afro-brasileira. Apresenta o termo moda afro-brasileira para falar de um novo segmento que surge com o ativismo de jovens negros e periféricos, que resgatam o legado da cultura e da resistência negra para comunicar uma consciência política por meio do vestir. Também revisita a música black e o hip-hop para exal-tar a luta de resistência de ourives e alfaiates negros que deram a sua contribuição ao campo do design e da moda nos séculos xvi, xvii e xviii, cujos fazeres jamais foram reconhecidos. E assim como toda luta negra parte de movimentos sociais dos negros, esta obra termina com um discurso proferido pela autora na abertura do GT 6 – Moda Afro-brasileira e Ativismo no Colóquio de Moda 2021.