bluuebunny/crossref_metadata_2025 huggingface dataset:
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
Authors: Anand Aditya , Adithya Solai , Rustagi Swapnil , Seth Priyam , Sundaresan Vijay , Maier Daryl , Nandivada V. Krishna , Thakur Manas
Published: June 2024

The runtimes of managed object-oriented languages such as Java allocate objects on the heap, and rely on automatic garbage collection (GC) techniques for freeing up unused objects. Most such runtimes also consist of just-in-time (JIT) compilers that optimize memory access and GC times by employing escape analysis: an object that does not escape (outlive) its allocating method can be allocated on (and freed up with) the stack frame of the corresponding method. However, in order to minimize the time spent in JIT compilation, the scope of such useful analyses is quite limited, thereby restricting their precision significantly. On the contrary, even though it is feasible to perform precise program analyses statically, it is not possible to use their results in a managed runtime without a closed-world assumption. In this paper, we propose a static+dynamic scheme that allows one to harness the results of a precise static escape analysis for allocating objects on stack, while taking care of both soundness and efficiency concerns in the runtime.

Our scheme comprises of three key ideas. First, using the results of a statically performed escape analysis, it performs optimistic stack allocation during JIT compilation. Second, it handles the challenges associated with features that may invalidate the optimism, using a novel idea of dynamic heapification. Third, it uses another novel notion of stack ordering, again supported by a static analysis, to reduce the overheads associated with the checks that determine the need for heapification. The static and the runtime components of our approach are implemented in the Soot optimization framework and in the tiered infrastructure of the Eclipse OpenJ9 VM, respectively. To evaluate the benefits, we compare our scheme with the existing escape analysis and find that it succeeds in allocating a much larger number of objects on the stack. Furthermore, the enhanced stack allocation leads to a significant reduction in the number of GC cycles and brings decent performance improvements, especially suited for constrained-memory environments.
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
Authors: Yao Peisen , Zhou Jinguo , Xiao Xiao , Shi Qingkai , Wu Rongxin , Zhang Charles
Published: June 2024

This paper presents a scalable path- and context-sensitive data dependence analysis. The key is to address the aliasing-path-explosion problem when enforcing a path-sensitive memory model. Specifically, our approach decomposes the computational efforts of disjunctive reasoning into 1) a context- and semi-path-sensitive analysis that concisely summarizes data dependence as the symbolic and storeless value-flow graphs, and 2) a demand-driven phase that resolves transitive data dependence over the graphs, piggybacking the computation of fully path-sensitive pointer information with the resolution of data dependence of interest. We have applied the approach to two clients, namely thin slicing and value-flow bug finding. Using a suite of 16 C/C++ programs ranging from 13 KLoC to 8 MLoC, we compare our techniques against a diverse group of state-of-the-art analyses, illustrating the significant precision and scalability advantages of our approach.
Allo: A Programming Model for Composable Accelerator Design
Authors: Chen Hongzheng , Zhang Niansong , Xiang Shaojie , Zeng Zhichen , Dai Mengjia , Zhang Zhiru
Published: June 2024

Special-purpose hardware accelerators are increasingly pivotal for sustaining performance improvements in emerging applications, especially as the benefits of technology scaling continue to diminish. However, designers currently lack effective tools and methodologies to construct complex, high-performance accelerator architectures in a productive manner. Existing high-level synthesis (HLS) tools often require intrusive source-level changes to attain satisfactory quality of results. Despite the introduction of several new accelerator design languages (ADLs) aiming to enhance or replace HLS, their advantages are more evident in relatively simple applications with a single kernel. Existing ADLs prove less effective for realistic hierarchical designs with multiple kernels, even if the design hierarchy is flattened.

In this paper, we introduce Allo, a composable programming model for efficient spatial accelerator design. Allo decouples hardware customizations, including compute, memory, communication, and data type from algorithm specification, and encapsulates them as a set of customization primitives. Allo preserves the hierarchical structure of an input program by combining customizations from different functions in a bottom-up, type-safe manner. This approach facilitates holistic optimizations that span across function boundaries. We conduct comprehensive experiments on commonly-used HLS benchmarks and several realistic deep learning models. Our evaluation shows that Allo can outperform state-of-the-art HLS tools and ADLs on all test cases in the PolyBench. For the GPT2 model, the inference latency of the Allo generated accelerator is 1.7x faster than the NVIDIA A100 GPU with 5.4x higher energy efficiency, demonstrating the capability of Allo to handle large-scale designs.
Mechanised Hypersafety Proofs about Structured Data
Authors: Gladshtein Vladimir , Zhao Qiyuan , Ahrens Willow , Amarasinghe Saman , Sergey Ilya
Published: June 2024

Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of manipulations with such structured data is challenging, as they are often composed of multiple loops with non-trivial invariants. In this work, we observe that specifications for structured data manipulations can be phrased as hypersafety properties, i.e., predicates that relate traces of
k
programs. To turn this observation into an effective verification methodology, we developed the Logic for Graceful Tensor Manipulation (LGTM), a new Hoare-style relational separation logic for specifying and verifying computations over structured data. The key enabling idea of LGTM is that of parametrised hypersafety specifications that allow the number
k
of the program components to depend on the program variables. We implemented LGTM as a foundational embedding into Coq, mechanising its rules, meta-theory, and the proof of soundness. Furthermore, we developed a library of domain-specific tactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts that enjoy a high degree of reuse. We argue for the effectiveness of relational reasoning about structured data in LGTM by specifying and mechanically proving correctness of 13 case studies including computations on compressed arrays and efficient operations over multiple kinds of sparse tensors.
Automated Verification of Fundamental Algebraic Laws
Authors: Zakhour George , Weisenburger Pascal , Salvaneschi Guido
Published: June 2024

Algebraic laws of
functions in mathematics
– such as commutativity, associativity, and idempotence – are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of
functions in coding
, however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack built-in mechanisms to enforce and verify that operations adhere to such properties.

In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five state-of-the-art verifiers on a total of 142 instances of algebraic properties shows that Propel is able to automatically deduce algebraic properties in different domains that rely on such properties for correctness, even in cases where competitors fail to verify the same properties or time out.
From Batch to Stream: Automatic Generation of Online Algorithms
Authors: Wang Ziteng , Pailoor Shankara , Prakash Aaryan , Wang Yuepeng , Dillig Işıl
Published: June 2024

Online streaming algorithms, tailored for continuous data processing, offer substantial benefits but are often more intricate to design than their offline counterparts. This paper introduces a novel approach for automatically synthesizing online streaming algorithms from their offline versions. In particular, we propose a novel methodology, based on the notion of relational function signature (RFS), for deriving an online algorithm given its offline version. Then, we propose a concrete synthesis algorithm that is an instantiation of the proposed methodology. Our algorithm uses the RFS to decompose the synthesis problem into a set of independent subtasks and uses a combination of symbolic reasoning and search to solve each subproblem. We implement the proposed technique in a new tool called Opera and evaluate it on over 50 tasks spanning two domains: statistical computations and online auctions. Our results show that Opera can automatically derive the online version of the original algorithm for 98% of the tasks. Our experiments also demonstrate that Opera significantly outperforms alternative approaches, including adaptations of SyGuS solvers to this problem as well as two of Opera's own ablations.
Wavefront Threading Enables Effective High-Level Synthesis
Authors: Pelton Blake , Sapek Adam , Eguro Ken , Lo Daniel , Forin Alessandro , Humphrey Matt , Xi Jinwen , Cox David , Karandikar Rajas , de Fine Licht Johannes , Babin Evgeny , Caulfield Adrian , Burger Doug
Published: June 2024

Digital systems are growing in importance and computing hardware is growing more heterogeneous. Hardware design, however, remains laborious and expensive, in part due to the limitations of conventional hardware description languages (HDLs) like VHDL and Verilog. A longstanding research goal has been programming hardware like software, with high-level languages that can generate efficient hardware designs. This paper describes Kanagawa, a language that takes a new approach to combine the programmer productivity benefits of traditional High-Level Synthesis (HLS) approaches with the expressibility and hardware efficiency of Register-Transfer Level (RTL) design. The language's concise syntax, matched with a hardware design-friendly execution model, permits a relatively simple toolchain to map high-level code into efficient hardware implementations.
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
Authors: Gäher Lennard , Sammler Michael , Jung Ralf , Krebbers Robbert , Dreyer Derek
Published: June 2024

Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a general-purpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code.
Verification under Intel-x86 with Persistency
Authors: Abdulla Parosh , Atig Mohamed Faouzi , Bouajjani Ahmed , Kumar K. Narayan , Saivasan Prakash
Published: June 2024

The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
Authors: Zhou Zhe , Ye Qianchuan , Delaware Benjamin , Jagannathan Suresh
Published: June 2024

Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library.

In this paper, we consider the specification and verification of such representation invariants using symbolic finite automata (SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries. To facilitate modular and compositional reasoning, we integrate SFAs into a refinement type system to qualify stateful computations resulting from such interactions. The particular instantiation we consider, Hoare Automata Types (HATs), allows us to both specify and automatically type-check the representation invariants of a datatype, even when its implementation depends on stateful library methods that operate over hidden state.

We also develop a new bidirectional type checking algorithm that implements an efficient subtyping inclusion check over HATs, enabling their translation into a form amenable for SMT-based automated verification. We present extensive experimental results on an implementation of this algorithm that demonstrates the feasibility of type-checking complex and sophisticated HAT-specified OCaml data structure implementations layered on top of stateful library APIs.
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
Authors: Albert Elvira , Garcia de la Banda Maria , Hernández-Cerezo Alejandro , Ignatiev Alexey , Rubio Albert , Stuckey Peter J.
Published: June 2024

Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed, and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named SuperStack, which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.
Compiling Conditional Quantum Gates without Using Helper Qubits
Authors: Huang Keli , Palsberg Jens
Published: June 2024

We present a compilation scheme for conditional quantum gates. Our scheme compiles a multi-qubit conditional to a linear number of two-qubit conditionals. This can be done straightforwardly with helper qubits, but we show how to do it without using helper qubits and with much fewer gates than in previous work. Specifically, our scheme requires 1/3 as many gates as the previous best scheme without using helper qubits, which is essential for practical use. Our experiments show that several quantum-circuit optimizers have little impact on the compiled code from the previous best scheme, confirming the need for our new scheme. Our experiments with Grover's algorithm and quantum walk also show that our scheme has a major impact on the reliability of the compiled code.
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
Authors: Parthasarathy Gaurav , Dardinier Thibault , Bonneau Benjamin , Müller Peter , Summers Alexander J.
Published: June 2024

Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its
actual implementation
, not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.
Bringing the WebAssembly Standard up to Speed with SpecTec
Authors: Youn Dongjun , Shin Wonho , Lee Jaehyun , Ryu Sukyoung , Breitner Joachim , Gardner Philippa , Lindley Sam , Pretnar Matija , Rao Xiaojia , Watt Conrad , Rossberg Andreas
Published: June 2024

WebAssembly (Wasm) is a portable low-level bytecode language and virtual machine that has seen increasing use in a variety of ecosystems. Its specification is unusually rigorous – including a full formal semantics for the language – and every new feature must be specified in this formal semantics, in prose, and in the official reference interpreter before it can be standardized. With the growing size of the language, this manual process with its redundancies has become laborious and error-prone, and in this work, we offer a solution. We present SpecTec, a domain-specific language (DSL) and toolchain that facilitates both the Wasm specification and the generation of artifacts necessary to standardize new features. SpecTec serves as a single source of truth — from a SpecTec definition of the Wasm semantics, we can generate a typeset specification, including formal definitions and prose pseudocode descriptions, and a meta-level interpreter. Further backends for test generation and interactive theorem proving are planned. We evaluate SpecTec’s ability to represent the latest Wasm 2.0 and show that the generated meta-level interpreter passes 100% of the applicable official test suite. We show that SpecTec is highly effective at discovering and preventing errors by detecting historical errors in the specification that have been corrected and ten errors in five proposals ready for inclusion in the next version of Wasm. Our ultimate aim is that SpecTec should be adopted by the Wasm standards community and used to specify future versions of the standard.
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Authors: Igarashi Atsushi , Ozaki Shota , Sekiyama Taro , Tanabe Yudai
Published: June 2024

Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficiency problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop λC

mp

, which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present λS

mp

, a space-efficient version of λC

mp

, and prove that λS

mp

programs can be executed in a space-efficient manner and that translation from λC

mp

to λS

mp

is type- and semantics-preserving.
Quest Complete: The Holy Grail of Gradual Security
Authors: Chen Tianyu , Siek Jeremy G.
Published: June 2024

Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behave the same modulo cast errors. Unfortunately, Toro et al. [2018] identify a tension between the gradual guarantee and information security; they were unable to satisfy both properties in the language GSLRef and had to settle for only satisfying information-flow security. Azevedo de Amorim et al. [2020] show that by sacrificing type-guided classification, one obtains a language that satisfies both noninterference and the gradual guarantee. Bichhawat et al. [2021] show that both properties can be satisfied by sacrificing the no-sensitive-upgrade mechanism, replacing it with a static analysis.

In this paper we present a language design, 𝜆★IFC, that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of GSLRef and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of 𝜆★IFC is to walk back the decision in GSLRef to include the unknown label ★ among the runtime security labels. We give a formal definition of 𝜆★IFC, prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of 𝜆★IFC is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein), thereby expanding the coercion-based theory of gradual typing.
Compiling Probabilistic Programs for Variable Elimination with Information Flow
Authors: Li Jianlin , Wang Eric , Zhang Yizhou
Published: June 2024

A key promise of probabilistic programming is the ability to specify rich models using an expressive program- ming language. However, the expressive power that makes probabilistic programming languages enticing also poses challenges to inference, so much so that specialized approaches to inference ban language features such as recursion. We present an approach to variable elimination and marginal inference for probabilistic programs featuring bounded recursion, discrete distributions, and sometimes continuous distributions. A compiler eliminates probabilistic side effects, using a novel information-flow type system to factorize probabilistic computations and hoist independent subcomputations out of sums or integrals. For a broad class of recursive programs with dynamically recurring substructure, the compiler effectively decomposes a global marginal-inference problem, which may otherwise be intractable, into tractable subproblems. We prove the compilation correct by showing that it preserves denotational semantics. Experiments show that the compiled programs subsume widely used PTIME algorithms for recursive models and that the compilation time scales with the size of the inference problems. As a separate contribution, we develop a denotational, logical-relations model of information-flow types in the novel measure-theoretic setting of probabilistic programming; we use it to prove noninterference and consequently the correctness of variable elimination.
Predictable Verification using Intrinsic Definitions
Authors: Murali Adithya , Rivera Cody , Madhusudan P.
Published: June 2024

We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.
Context-Free Language Reachability via Skewed Tabulation
Authors: Lei Yuxiang , Bossut Camille , Sui Yulei , Zhang Qirun
Published: June 2024

Context-free language reachability (CFL-reachability) is a prominent model for formulating program analysis problems. Almost all CFL-reachability algorithms are based on the Reps-Horwitz-Sagiv (RHS) tabulation. In essence, the RHS tabulation, based on normalized context-free grammars, is similar to the CYK algorithm for CFL-parsing. Consider a normalized rule S ::= A B and a CFL-reachability problem instance of computing S-edges in the input graph. The RHS tabulation obtains all summary edges (i.e., S-, A-, and B-edges) based on the grammar rules. However, many A- and B-edges are wasted because only a subset of those edges eventually contributes to generating S-edges in the input graph.

This paper proposes a new tabulation strategy for speeding up CFL-reachability by eliminating wasted and unnecessary summary edges. We particularly focus on recursive nonterminals. Our key technical insight is that the wasted edge generations and insertions caused by recursive nonterminals can be avoided by modifying the parse trees either statically (by transforming the grammar) or dynamically (using a specialized online CFL-reachability solver). For example, if a recursive nonterminal B, generated by a rule B ::= B X, appears on the right-hand side of a rule S ::= A B, we can make S recursive (by introducing a new rule S ::= S X) and eliminate the original recursive rule (B ::= B X). Due to the rule S ::= S X, the shapes of the parse trees associated with the left-hand-side nonterminal S become more "skewed". Thus, we name our approach skewed tabulation for CFL-reachability.

Skewed tabulation can significantly improve the scalability of CFL-reachability by reducing wasted and unnecessary summary edges. We have implemented skewed tabulation and applied the corresponding CFL-reachability algorithm to an alias analysis, a value-flow analysis, and a taint analysis. Our extensive evaluation based on SPEC 2017 benchmarks yields promising results. For the three client analyses, CFL-reachability based on skewed tabulation can achieve 3.34×, 1.13× and 2.05× speedup over the state-of-the-art RHS-tabulation-based CFL-reachability solver and consume 60.05%, 20.38% and 63.06% less memory, respectively. Furthermore, the cost of grammar transformation for skewed tabulation is negligible, typically taking less than one second.
Equivalence by Canonicalization for Synthesis-Backed Refactoring
Authors: Lubin Justin , Ferguson Jeremy , Ye Kevin , Yim Jacob , Chasins Sarah E.
Published: June 2024

We present an enumerative program synthesis framework called
component-based refactoring
that can refactor "direct" style code that does not use library components into equivalent "combinator" style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code called
equivalence by canonicalization
that does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such as and in the statically-typed functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool called Cobbler and evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.
Hashing Modulo Context-Sensitive 𝛼-Equivalence
Authors: Blaauwbroek Lasse , Olšák Miroslav , Geuvers Herman
Published: June 2024

The notion of α-equivalence between λ-terms is commonly used to identify terms that are considered equal. However, due to the primitive treatment of free variables, this notion falls short when comparing subterms occurring within a larger context. Depending on the usage of the Barendregt convention (choosing different variable names for all involved binders), it will equate either too few or too many subterms. We introduce a formal notion of context-sensitive α-equivalence, where two open terms can be compared within a context that resolves their free variables. We show that this equivalence coincides exactly with the notion of bisimulation equivalence. Furthermore, we present an efficient
O
(
n
log
n
) runtime hashing scheme that identifies λ-terms modulo context-sensitive α-equivalence, generalizing over traditional bisimulation partitioning algorithms and improving upon a previously established
O
(
n
log
2
n
) bound for a hashing modulo ordinary α-equivalence by Maziarz et al. Hashing λ-terms is useful in many applications that require common subterm elimination and structure sharing. We hav employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.
Structural Properties on Scale-Free Tree Network with an Ultra-Large Diameter
Authors: Ma Fei , Wang Ping
Published: June 2024

Scale-free networks are prevalently observed in a great variety of complex systems, which triggers various researches relevant to networked models of such type. In this work, we propose a family of growth tree networks

\(\mathcal{T}_{t}\)

, which turn out to be scale-free, in an iterative manner. As opposed to most of published tree models with scale-free feature, our tree networks have the power-law exponent

\(\gamma=1{ + }\ln 5/\ln 2\)

that is obviously larger than

\(3\)

. At the same time, “small-world” property can not be found particularly because models

\(\mathcal{T}_{t}\)

have an ultra-large diameter

\(D_{t}\)

(i.e.,

\(D_{t}\sim|\mathcal{T}_{t}|^{\ln 3/\ln 5}\)

) and a greater average shortest path length

\(\langle\mathcal{W}_{t}\rangle\)

(namely,

\(\langle\mathcal{W}_{t}\rangle\sim|\mathcal{T}_{t}|^{\ln 3/\ln 5}\)

) where

\(|\mathcal{T}_{t}|\)

represents vertex number. Next, we determine Pearson correlation coefficient and verify that networks

\(\mathcal{T}_{t}\)

display disassortative mixing structure. In addition, we study random walks on tree networks

\(\mathcal{T}_{t}\)

and derive exact solution to mean hitting time

\(\langle\mathcal{H}_{t}\rangle\)

. The results suggest that the analytic formula for quantity

\(\langle\mathcal{H}_{t}\rangle\)

as a function of vertex number

\(|\mathcal{T}_{t}|\)

shows a power-law form, i.e.,

\(\langle\mathcal{H}_{t}\rangle\sim|\mathcal{T}_{t}|^{1+\ln 3/\ln 5}\)

. Accordingly, we execute extensive experimental simulations, and demonstrate that empirical analysis is in strong agreement with theoretical results. Lastly, we provide a guide to extend the proposed iterative manner in order to generate more general scale-free tree networks with large diameter.
Eg5 and Diseases: From the Well‐Known Role in Cancer to the Less‐Known Activity in Noncancerous Pathological Conditions
Authors: Ricci Alessia , Carradori Simone , Cataldi Amelia , Zara Susi
Published: June 2024

Eg5 is a protein encoded by KIF11 gene and is primarily involved in correct mitotic cell division. It is also involved in nonmitotic processes such as polypeptide synthesis, protein transport, and angiogenesis. The scientific literature sheds light on the ubiquitous functions of KIF11 and its involvement in the onset and progression of different pathologies. This review focuses attention on two main points: (1) the correlation between Eg5 and cancer and (2) the involvement of Eg5 in noncancerous conditions. Regarding the first point, several tumors revealed an overexpression of this kinesin, thus pushing to look for new Eg5 inhibitors for clinical practice. In addition, the evaluation of Eg5 expression represents a crucial step, as its overexpression could predict a poor prognosis for cancer patients. Referring to the second point, in specific pathological conditions, the reduced activity of Eg5 can be one of the causes of pathological onset. This is the case of Alzheimer’s disease (AD), in which Aβ and Tau work as Eg5 inhibitors, or in acquired immune deficiency syndrome (AIDS), in which Tat‐mediated Eg5 determines the loss of CD4+ T‐lymphocytes. Reduced Eg5 activity, due to mutations of KIF11 gene, is also responsible for pathological conditions such as microcephaly with or without chorioretinopathy, lymphedema, or intellectual disability (MCLRI) and familial exudative vitreous retinopathy (FEVR). In conclusion, this review highlights the double impact that overexpression or loss of function of Eg5 could have in the onset and progression of different pathological situations. This emphasizes, on one hand, a possible role of Eg5 as a potential biomarker and new target in cancer and, on the other hand, the promotion of Eg5 expression/activity as a new therapeutic strategy in different noncancerous diseases.
Discovery Patterns of Drugs Approved for Treating Bipolar Disorder by Applying Operational Criteria of Serendipity: A Historical Analysis
Authors: López-Muñoz Francisco , D’Ocón Pilar , Romero Alejandro , Guerra José A. , De Berardis Domenico , Álamo Cecilio
Published: June 2024

While the scientific community has long acknowledged the significant role of serendipity in shaping the field of contemporary psychopharmacology, its impact has not undergone a comprehensive analysis using operational methodologies. Serendipity, originally defined as discoveries stemming from a blend of luck and astuteness by Walpole, has been operationalized by our research group. Our definition builds upon Walpole’s notion of fortuitous accidents and keen insight leading to the unexpected revelation of something unintended. We have discerned four unique serendipitous attributability patterns. In this paper, we delve into the historical aspect of how serendipity has played a role in the discovery and advancement of drugs approved for addressing different stages of bipolar disorder. The revelation of valproate’s antimanic properties aligns with the pure serendipitous pattern (type I). Conversely, the discovery of lithium’s antimanic effects corresponds to the mixed type II pattern, where the initial serendipitous observation of sedation in research animals, prompted by adding lithium salts to enhance uric acid solubility, led to the planned discovery of its calming impact on manic patients. On the contrary, the recognition of the mood‐stabilizing attributes of lamotrigine aligns with the type III archetype. This particular pattern is defined by serendipity emerging as a consequence of a discovery that was initially nonserendipitous, as mood‐stabilizing efficacy was incidentally observed during the treatment of epileptic patients for whom the drug was originally developed. Finally, carbamazepine and, notably, atypical antipsychotics fall within the type IV pattern. In this category, serendipity is entirely absent, as the antimanic use of carbamazepine was a straightforward extension of the use of other antiepileptic drugs. Atypical antipsychotics were introduced into bipolar disorder therapy through a deliberate and targeted design process, seeking drugs capable of acting on specific biological targets.
Supplementary Figure 19 from Ultrasensitive Detection of Circulating LINE-1 ORF1p as a Specific Multicancer Biomarker
Authors: Taylor Martin S. , Wu Connie , Fridy Peter C. , Zhang Stephanie J. , Senussi Yasmeen , Wolters Justina C. , Cajuso Tatiana , Cheng Wen-Chih , Heaps John D. , Miller Bryant D. , Mori Kei , Cohen Limor , Jiang Hua , Molloy Kelly R. , Chait Brian T. , Goggins Michael G. , Bhan Irun , Franses Joseph W. , Yang Xiaoyu , Taplin Mary-Ellen , Wang Xinan , Christiani David C. , Johnson Bruce E. , Meyerson Matthew , Uppaluri Ravindra , Egloff Ann Marie , Denault Elyssa N. , Spring Laura M. , Wang Tian-Li , Shih Ie-Ming , Fairman Jennifer E. , Jung Euihye , Arora Kshitij S. , Yilmaz Osman H. , Cohen Sonia , Sharova Tatyana , Chi Gary , Norden Bryanna L. , Song Yuhui , Nieman Linda T. , Pappas Leontios , Parikh Aparna R. , Strickland Matthew R. , Corcoran Ryan B. , Mustelin Tomas , Eng George , Yilmaz Ömer H. , Matulonis Ursula A. , Chan Andrew T. , Skates Steven J. , Rueda Bo R. , Drapkin Ronny , Klempner Samuel J. , Deshpande Vikram , Ting David T. , Rout Michael P. , LaCava John , Walt David R. , Burns Kathleen H.
Published: June 2024

Assay validation for second-generation ORF1p Simoa assays.
Supplementary Figure S7 from The TERT Promoter is Polycomb-Repressed in Neuroblastoma Cells with Long Telomeres
Authors: Graham Mindy K. , Xu Beisi , Davis Christine , Meeker Alan K. , Heaphy Christopher M. , Yegnasubramanian Srinivasan , Dyer Michael A. , Zeineldin Maged
Published: June 2024

Supplementary Figure S7
Igreja e Estado: o sentido da pastoral de 1860 do Arcebispo da Bahia
Authors: Rosário Adalgisa Maria V. do , Monteiro Hamilton de Mattos
Published: June 2024

Analysis of the Pastoral letter of the Archbishop of Bahia, dated of 1860, and its place in the general context of the great crisis of northeastern agriculture and the relations between the State and agricultural workers.
Um empresário nas milícias paulistas: o Brigadeiro Luís Antonio de Souza
Authors: Leonzo Nanci
Published: June 2024

The author, in this paper, studies the participation of Brigadier Luís Antonio de Souza, a very important personality, of Portuguese origin, who lived in the old São Paulo Capitania, in the military organization named Milícias, formed by the male population considered apt to render free military Service.
Memorias subterráneas y mecanismos de censura: Exposiciones de arte, ‘El Tercer Mundo’ en Venezuela y ‘Queermuseu’ en Brasil
Authors: Quiroz Jair Jose Gauna
Published: June 2024

Censorship occurs in contexts where dominant discourses establish the invisibility of subterranean memories; thus, artworks act as vehicles of memories by their external symbols. The research presents case studies on the censorship of the individual exhibition ‘El Tercer Mundo’ by MAx Provenzano at the Museum of Art in Valencia, Venezuela, and the unexpected closure of the collective exhibition ‘Queermuseu: Cartografias da diferença na arte brasileira’ at the Santander Cultural in Brazil, in the years 2015 and 2017, respectively. The mechanisms of censorship were analyzed to identify subterranean memories in art exhibitions, as discursive practices to determine control over cultural memory through power conflicts. Furthermore, discursive and ideological formations were analyzed to understand the elements behind the acts of censorship, in order to understand divergent narratives reflecting on the different identities and memories of Latin American regions.
A Geografia em ação: as lógicas de colonização do território brasileiro a partir das controvérsias epistemológicas sobre a nova localização da sua capital (1947-1955)
Authors: Lira Larissa Alves de
Published: June 2024

This article analyses the reflections of a group of geographers on the choice of the new location for Brasília and the regional planning logic. Two scientific comissions held meetings in 1947 at the Brazilian Institute of Geography and Statistics (IBGE) and the National Geography Council (CNG) to explore the Brazilian Central Plateau and discuss the new location. French geomorphologist Francis Ruellan led the first meeting and Leo Waibel, an economic geographer born in Germany and naturalized in the United States led the other. These two leaderships represented different sides of technical-scientific controversies. Inspired by Bruno Latour’s methodology, controversies are seen as a possibility to observe clear colonization and political projects for Brazil in opposition, as well as geography’s performativity, its ability to build territories. The question that guided this research was: by which epistemological logic was Brazil colonized?
Meditações sobre a terra: a geografia de Byung-Chul Han
Authors: Nascimento Francyjonison Custodio do
Published: June 2024

Há tempos, a Geografia busca contato com outras áreas do saber. Das artes e outras ciências até a Filosofia, os contatos são intensos e promovem novas articulações teóricas. Partindo desse pressuposto, o artigo promove o contato entre a Geografia e a obra de Byung-Chul Han, um filósofo germano-coreano contemporâneo. O trabalho, então, estabelece um esforço teórico de relacionar a noção de Terra do autor germano-coreano, presente no livro Louvor à Terra, às mais diversas tradições geográficas, pontuando como a Filosofia de Han dialoga vividamente com a Geografia e outras ciências sociais. Conclui-se que a obra, ao propor uma postura de consciência planetária, remodela compreensões, criticando a visão de Terra como recurso e reivindicando uma postura afetiva, que reconhece seu mistério e sua poesia ao associar o fazer científico ao encantamento.
O “sentido da vida” em Schopenhauer e Nietzsche
Authors: Paula Wander Andrade de
Published: June 2024

This is the first of two papers that aim to discuss the problem of the meaning of life in 19th century German philosophy, in order to open a dialogue with important discussions of contemporary philosophy. For this purpose, in this paper, the historical-philosophically problem is located (1); then, it investigates to what extent it is closely related, in the thoughts of Schopenhauer (2) and Nietzsche (3), to the themes of philosophical pessimism and nihilism; finally, it conclusively indicates the importance of both authors in establishing the problem in the philosophical tradition (4).
Arte e técnica no pensamento de Martin Heidegger
Authors: Rosa Felipe Seelaender Costa
Published: June 2024

With the following article we intend to investigate the relation of ambiguity between art and technique in the thought of Martin Heidegger. Having as main references the texts Die Frage nach der Technik e and Die Ursprüng des Kunstwerkes the main objective is to understand the two sides of this relation, since in Heideggerian thought these two dimensions have fundamental differences, but a common origin and meaning that can be thought from their Greek origin. Therefore, we attempt to underline the radicality of the thought effort proposed by Heidegger based on its circular aspect.