bluuebunny/crossref_metadata_2025 huggingface dataset:
Turning the Spyglass of Anthropology to Tackle Football
Authors: Canada Tracie
Published: January 2025

Drawing on almost a decade of immersive research with Black college football players, I argue that an anthropological and ethnographic approach to tackle football can complement studies in kinesiology by acknowledging the humanity, personhood, and lived experiences of athletes. In this article, I turn Zora Neale Hurston’s spyglass of Black feminist anthropology to football and center my disciplinary training to explain anthropology’s utility when studying this sport at the college level and the experiences of its Black participants. In particular, I highlight how my own positionality as a scholar mattered during my research experiences and how Black feminist anthropology provided me with the lens to consider care in football beyond just medical care performed to support the physical body. I make the case for how, through the spyglass of anthropological and ethnographic examination, the structural and the experiential of tackle football can be observed in tandem.
Supplemental Material: Ultra-high temperatures recorded in parental magmas from hybrid zones
Authors: Rodríguez Carmen , al. et
Published: January 2025

Tables S1–S6 and technical and analytical details (Text S1).
Induction of macrophage efferocytosis in pancreatic cancer via PI3Kγ inhibition and radiotherapy promotes tumour control
Authors: Russell Shannon Nicole , Demetriou Constantinos , Valenzano Giampiero , Evans Alice , Go Simei , Stanly Tess , Hazini Ahmet , Willenbrock Frances , Gordon-Weeks Alex Nicolas , Mukherjee Somnath , Tesson Matthias , Morton Jennifer P , O'Neill Eric , Jones Keaton Ian
Published: January 2025

Background

The immune suppression mechanisms in pancreatic ductal adenocarcinoma (PDAC) remain unknown, but preclinical studies have implicated macrophage-mediated immune tolerance. Hence, pathways that regulate macrophage phenotype are of strategic interest, with reprogramming strategies focusing on inhibitors of phosphoinositide 3-kinase-gamma (PI3Kγ) due to restricted immune cell expression. Inhibition of PI3Kγ alone is ineffective in PDAC, despite increased infiltration of CD8+ T cells.

Objective

We hypothesised that the immune stimulatory effects of radiation, and its ability to boost tumour antigen availability could synergise with PI3Kγ inhibition to augment antitumour immunity.

Design

We used orthoptic and genetically engineered mouse models of pancreatic cancer (LSL-KrasG12D/+;Trp53R172H/+;Pdx1-Cre). Stereotactic radiotherapy was delivered using contrast CT imaging, and PI3Kγ inhibitors by oral administration. Changes in the tumour microenvironment were quantified by flow cytometry, multiplex immunohistochemistry and RNA sequencing. Tumour-educated macrophages were used to investigate efferocytosis, antigen presentation and CD8+ T cell activation. Single-cell RNA sequencing data and fresh tumour samples with autologous macrophages to validate our findings.

Results

Tumour-associated macrophages that employ efferocytosis to eradicate apoptotic cells can be redirected to present tumour antigens, stimulate CD8+ T cell responses and increase local tumour control. Specifically, we demonstrate how PI3Kγ signalling restricts inflammatory macrophages and that inhibition supports MERTK-dependent efferocytosis. We further find that the combination of PI3Kγ inhibition with targeted radiotherapy stimulates inflammatory macrophages to invoke a pathogen-induced like efferocytosis that switches from immune tolerant to antigen presenting.

Conclusions

Our data supports a new immunotherapeutic approach and a translational rationale to improve survival in PDAC.
LGR5 as a diagnostic marker for dysplasia in serrated polyps
Authors: Yilmaz Osman , Arora Kshtij , Lee Soo Hyun , Hosseini Sahar , Chen Feidi , Padmanabha Nandan , Eng George , Kantekure Kanchan , Yilmaz Omer , Deshpande Vikram
Published: January 2025

Aims

WNT signalling pathway dysregulation is often a critical early component in colorectal neoplasia, particularly the chromosomal instability pathway. Using two WNT reporters,LGR5andAXIN2, we sought to assess whether these polyps demonstrate predictable expression patterns and if these patterns show diagnostic value.

Methods

We evaluated 23 adenomas (TA), 23 sessile serrated lesions (SSLs), 14 SSL with dysplasia and 38 traditional serrated adenomas (TSA). Chromogenic in situ hybridisation stains (ISH) forLGR5andAXIN2were performed. Reactivity was defined as strong, intermediate or weak. Upper third crypt reactivity was defined as full-thickness staining. Accentuation within ectopic crypts (ECF) was recorded.

Results

TAs (91%) showed strong reactivity and full-thickness staining withLGR5. TSAs showed full-thickness and weak to intermediateLGR5reactivity (79%) and ECF withLGR5accentuation was exclusively seen in TSA. SSL showed weakLGR5reactivity confined to the basal crypt region (100%). SSL with dysplasia also showed weak or intermediate (100%)LGR5reactivity, but the reactivity pattern was full thickness (88%).AXIN2expression parallelsLGR5expression (Pearson coefficient=0.63) regarding signal intensity for the examined polyp groups.

Conclusions

Qualitative and quantitative differences inAXIN2andLGR5expression assist in the diagnosis of SSL with dysplasia.
Timing-based mass measurement of exotic long-lived particles at the FCC-ee
Authors: Aleksan R. , Perez E. , Polesello G. , Valle N.
Published: January 2025

The very high luminosity run foreseen at the Z-pole for the FCC-ee will allow the detection in Z decays of new particles with very low couplings to the Standard Model. These particles can have measurable flight paths before they decay. If the timing and the position of the decay vertex can be measured with high precision, the mass of such particles can be measured by exploiting the constrained kinematics of an $$e^+e^-$$

e
+

e
-

collider. The mass resolution achievable with this technique is studied through a detailed analysis in the framework of a parametrised simulation of the performance of the IDEA detector. The adopted benchmark model is the production of Heavy Neutral Leptons, which is one of the key channels for new physics discovery at the FCC-ee.
Diagnosis Method for Abnormal Data in Bridge Health Monitoring Using BMA-Assisted EasyEnsemble-AlexNet
Authors: Xin Jingzhou , Wang Chen , Xia Meng , Tang Qizhi , Jiang Yan , Zhang Hong , Zhou Jianting
Published: January 2025

Abnormal data diagnosis in the bridge health monitoring (BHM) system is of great significance to improve the credibility of structural safety assessment. However, a notable imbalance exists between the number of abnormal and normal samples in deep learning-based methods, resulting in a lower accuracy when identifying limited abnormal categories. To this end, this study proposes an abnormal data diagnosis method for BHM using EasyEnsemble, AlexNet and Bayesian model averaging (BMA). First, multiple balanced EasyEnsemble subsets are constructed from the training set by random sampling. Subsequently, each subset is used for the training of a single AlexNet model, and the posterior probability of each model is determined by calculating their log-likelihood on the training subset. Then, the prediction results of all models are combined by BMA according to their posterior probabilities. Finally, the effectiveness of this method is verified using data from a BHM system. The results show that the proposed method significantly strengthens the diagnosis performance of abnormal data, achieving an overall accuracy of 96.66%. Compared to traditional methods, the proposed method offers higher training efficiency and diagnosis accuracy with fewer samples, especially for similar abnormal categories.
On the one-dimensional representations of finite W-superalgebras for 𝔤𝔩M|N
Authors: Yang Fanlei , Zeng Yang
Published: January 2025

Let [Formula: see text] be the general linear Lie superalgebra over an algebraically closed field [Formula: see text] of characteristic zero. Fix an arbitrary even nilpotent element [Formula: see text] in [Formula: see text] and let [Formula: see text] be the finite [Formula: see text]-superalgebra associated to the pair [Formula: see text]. In this paper, we will give a complete classification of one-dimensional representations for [Formula: see text]. To achieve this, we use the tool of shifted super Yangians to determine the commutative quotients of the finite [Formula: see text]-superalgebras.
Wormhole formation with gravitational particle creation mechanism
Authors: Gohain Mrinnoy M. , Bhuyan Kalyan , Chetia Chayanika
Published: January 2025

In this paper, we explore the possibility of formation of a traversable wormhole in General Relativity supported by particle creation mechanism. The repulsive back-reaction pressure generated through this mechanism can be thought of as a source of sustaining a traversable wormhole. In the first part of this paper, we model a wormhole geometry by assuming an inverse powerlaw variation of particle creation pressure within the wormhole geometry, and the shape function for the wormhole is obtained, assuming a finite redshift function. By stabilizing the wormhole structure, based on the causality of sound-speed we obtained the existence range of the parameter [Formula: see text] associated with particle creation mechanism. The general shape function obtained is found to adhere to the feasibility conditions of a viable wormhole geometry. Then we studied the 2D and 3D embedding derived for the obtained shape function. In the second part of the paper, we followed the reverse approach of the aforementioned treatment, where we derived the particle creation pressures by assuming three commonly utilized toy shape-functions. The energy conditions are then investigated for all these cases. In essence, particle creation phenomena inside the wormhole may indeed provide for the possibility of sustenance of stable wormhole structure.
Exploring the Molecular Impact of Achillea arabica on Hepatocellular Carcinoma: A Computational Study
Authors: Akkaya Hatice , Özmaldar Aydın
Published: January 2025

Hepatocellular carcinoma, presenting a significant health challenge, requires innovative approaches for treatment and prevention. Therefore, this study aimed to comprehensively characterize the potential of compounds from Achillea arabica on the mTOR, Akt and ERK signaling pathways using in silico methods. The drug likeness and ADME/T properties of the compounds were investigated using online tools. Molecular docking and molecular dynamics simulations were used to examine the key interactions of the selected compounds with the mTOR, Akt and ERK target proteins along with the known inhibitors. Three phenolic compounds demonstrated a strong binding affinity as the top candidates. Compounds quercetin, luteolin and apigenin exhibit potential as nontoxic alternatives for hepatocellular carcinoma treatment, typically used as synthetic chemical inhibitors.
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Authors: Varatalu Ian Erik , Veanes Margus , Ernits Juhan
Published: January 2025

We present a tool and theory RE# for regular expression matching that is built on symbolic derivatives, does not use backtracking, and, in addition to the classical operators, also supports complement, intersection and restricted lookarounds. We develop the theory formally and show that the main matching algorithm has input-linear complexity both in theory as well as experimentally. We apply thorough evaluation on popular benchmarks that show that RE# is over 71% faster than the next fastest regex engine in Rust on the baseline, and outperforms all state-of-the-art engines on extensions of the benchmarks often by several orders of magnitude.
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Authors: Leißa Roland , Ullrich Marcel , Meyer Joachim , Hack Sebastian
Published: January 2025

Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations.

Optimizations should understand the primitive operations of the specific application domain and thus happen on that level.

Domain-specific languages (DSLs) fulfill these requirements.

However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure & boilerplate code must be reimplemented for each DSL compiler.

This paper presents MimIR, an extensible, higher-order intermediate representation.

At its core, MimIR is a pure type system and, hence, a form of a typed lambda calculus.

Developers can declare the signatures of new (domain-specific) operations, called "axioms".

An axiom can be the declaration of a function, a type constructor, or any other entity with a possibly polymorphic, polytypic, and/or dependent type.

This way, developers can extend MimIR at any low or high level and bundle them in a "plugin".

Plugins extend the compiler and take care of optimizing and lowering the plugins' axioms.

We show the expressiveness and effectiveness of MimIR in three case studies:

Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation.

We show that in all three studies, MimIR produces code that has state-of-the-art performance.
BiSikkel: A Multimode Logical Framework in Agda
Authors: Ceulemans Joris , Nuyts Andreas , Devriese Dominique
Published: January 2025

Embedding Multimode Type Theory (MTT) as a library enables the usage of additional reasoning principles in off-the-shelf proof assistants without risking soundness or compatibility. Moreover, by interpreting embedded MTT terms in an internally constructed model of MTT, we can extract programs and proofs to the metalanguage and obtain interoperability between the embedded language and the metalanguage. The existing Sikkel library for Agda achieves this for Multimode Simple Type Theory (MSTT) with an internal presheaf model of dependent MTT. In this work, we add, on top of the simply-typed layer, a logical framework in which users can write multimode proofs about multimode Sikkel programs, still in an off-the-shelf proof assistant. To this end, we carve out of MTT a new multimode logical framework µLF over MSTT and implement it on top of Sikkel, interpreting both in the existing internal model. In the process, we further extend and improve the original codebase for each of the three layers (syntax, semantics and extraction) of Sikkel. We demonstrate the use of µLF by proving some properties about functions manipulating guarded streams and by implementing an example involving parametricity predicates.
Flo: A Semantic Foundation for Progressive Stream Processing
Authors: Laddad Shadaj , Cheung Alvin , Hellerstein Joseph M. , Milano Mae
Published: January 2025

Streaming systems are present throughout modern applications, processing continuous data in real-time. Existing streaming languages have a variety of semantic models and guarantees that are often incompatible. Yet all these languages are considered "streaming"---what do they have in common? In this paper, we identify two general yet precise semantic properties: streaming progress and eager execution. Together, they ensure that streaming outputs are deterministic and kept fresh with respect to streaming inputs. We formally define these properties in the context of Flo, a parameterized streaming language that abstracts over dataflow operators and the underlying structure of streams. It leverages a lightweight type system to distinguish bounded streams, which allow operators to block on termination, from unbounded ones. Furthermore, Flo provides constructs for dataflow composition and nested graphs with cycles. To demonstrate the generality of our properties, we show how key ideas from representative streaming and incremental computation systems---Flink, LVars, and DBSP---have semantics that can be modeled in Flo and guarantees that map to our properties.
Program Logics à la Carte
Authors: Vistrup Max , Sammler Michael , Jung Ralf
Published: January 2025

Program logics have proven a successful strategy for verification of complex programs. By providing local reasoning and means of abstraction and composition, they allow reasoning principles for individual components of a program to be combined to prove guarantees about a whole program. Crucially, these components and their proofs can be reused. However, this reuse is only available once the program logic has been defined. It is a frustrating fact of the status quo that whoever defines a new program logic must establish every part, both semantics and proof rules, from scratch. In spite of programming languages and program logics typically sharing many core features, reuse is generally not available across languages. Even inside one language, if the same underlying operation appears in multiple language primitives, reuse is typically not possible when establishing proof rules for the program logic.

To enable reuse across and inside languages when defining complex program logics (and proving them sound), we serve program logics à la carte by combining program logic fragments for the various effects of the language. Among other language features, the menu includes shared state, concurrency, and non-determinism as reusable, composable blocks that can be combined to define a program logic modularly. Our theory builds on ITrees as a framework to express language semantics and Iris as the underlying separation logic; the work has been mechanized in the Coq proof assistant.
Finite-Choice Logic Programming
Authors: Martens Chris , Simmons Robert J. , Arntzenius Michael
Published: January 2025

Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints—there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables.

We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size.
Calculational Design of Hyperlogics by Abstract Interpretation
Authors: Cousot Patrick , Wang Jeffery
Published: January 2025

We design various logics for proving hyper properties of iterative programs by application of abstract interpretation principles. In part I, we design a generic, structural, fixpoint abstract interpreter parameterized by an algebraic abstract domain describing finite and infinite computations that can be instantiated for various operational, denotational, or relational program semantics. Considering semantics as program properties, we define a post algebraic transformer for execution properties (e.g. sets of traces) and a Post algebraic transformer for semantic (hyper) properties (e.g. sets of sets of traces), we provide corresponding calculuses as instances of the generic abstract interpreter, and we derive under and over approximation hyperlogics. In part II, we define exact and approximate semantic abstractions, and show that they preserve the mathematical structure of the algebraic semantics, the collecting semantics post, the hyper collecting semantics Post, and the hyperlogics. Since proofs by sound and complete hyperlogics require an exact characterization of the program semantics within the proof, we consider in part III abstractions of the (hyper) semantic properties that yield simplified proof rules. These abstractions include the join, the homomorphic, the elimination, the principal ideal, the order ideal, the frontier order ideal, and the chain limit algebraic abstractions, as well as their combinations, that lead to new algebraic generalizations of hyperlogics, including the ∀∃
∗
, ∀∀
∗
, and ∃∀
∗
hyperlogics.
Program Analysis via Multiple Context Free Language Reachability
Authors: Conrado Giovanna Kobus , Kjelstrøm Adam Husted , van de Pol Jaco , Pavlogiannis Andreas
Published: January 2025

Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from
x
to
y
?) is phrased as a language reachability problem on a graph
G
wrt a CFL
L
. However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis? In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension
d
and a rank
r
. Larger
d
and
r
yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem. Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed? We show that the problem takes
O
(
n

2
d
+1

) time on a graph of
n
nodes when
r
=1, and
O
(
n

d
(
r
+1)

) time when
r
>1. Moreover, we show that when
r
=1, even the simpler membership problem has a lower bound of
n

2
d

based on the Strong Exponential Time Hypothesis, while reachability for
d
=1 has a lower bound of
n
3
based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for
r
=1, our algorithm is optimal within a factor
n
for all levels of the hierarchy based on the dimension
d
(and fully optimal for
d
=1). We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. When combined with existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, while it has remarkable coverage (confirming 94.3% of the reachable pairs reported by the overapproximation) on the remaining 3. To our knowledge, this is the first report of high and provable coverage for this challenging benchmark set.
TensorRight: Automated Verification of Tensor Graph Rewrites
Authors: Arora Jai , Lu Sirui , Jain Devansh , Xu Tianfan , Houshmand Farzin , Phothilimthana Phitchaya Mangpo , Lesani Mohsen , Narayanan Praveen , Murthy Karthik Srinivasa , Bodik Rastislav , Sabne Amit , Mendis Charith
Published: January 2025

Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting. To fill this gap, we introduce TensorRight, the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, TensorRight DSL, to represent rewrite rules using a novel axis definition, called
aggregated-axis
, which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of TensorRight DSL. TensorRight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate TensorRight’s verification capabilities by implementing rewrite rules present in XLA’s algebraic simplifier. The results demonstrate that TensorRight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic,
bounded
-verification system can express only 18 of these rules.
A Modal Deconstruction of Löb Induction
Authors: Gratzer Daniel
Published: January 2025

We present a novel analysis of the fundamental Löb induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive Löb induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.
Verifying Quantum Circuits with Level-Synchronized Tree Automata
Authors: Abdulla Parosh Aziz , Chen Yo-Ga , Chen Yu-Fang , Holík Lukáš , Lengál Ondřej , Lin Jyun-Ao , Lo Fang-Yi , Tsai Wei-Lun
Published: January 2025

We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices, which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification, i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches. We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.
The Decision Problem for Regular First Order Theories
Authors: Mathur Umang , Mestel David , Viswanathan Mahesh
Published: January 2025

The
Entscheidungsproblem
, or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. In this work, we consider an extension of this problem to regular first-order
theories
, i.e., (infinite) regular sets of formulae. Building on the elegant classification of syntactic classes as decidable or undecidable for the classical decision problem, we show that some classes (specifically, the EPR and Gurevich classes), which are decidable in the classical setting, become undecidable for regular theories. On the other hand, for each of these classes, we identify a subclass that remains decidable in our setting, leaving a complete classification as a challenge for future work. Finally, we observe that our problem generalises prior work on automata-theoretic verification of uninterpreted programs and propose a semantic class of existential formulae for which the problem is decidable.
Linear and Non-linear Relational Analyses for Quantum Program Optimization
Authors: Amy Matthew , Lunderville Joseph
Published: January 2025

The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an
affine relation analysis
, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum
programs
with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for
non-linear
relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations — such as Clifford+t — we show that the
sum-over-paths
technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
Authors: Kobayashi Naoki
Published: January 2025

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Authors: Haselwarter Philipp G. , Li Kwing Hei , Aguirre Alejandro , Gregersen Simon Oddershede , Tassarotti Joseph , Birkedal Lars
Published: January 2025

Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state.

In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence. We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.
Automating Equational Proofs in Dirac Notation
Authors: Xu Yingte , Barthe Gilles , Zhou Li
Published: January 2025

Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski's theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature.
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Authors: Stassen Philipp , Møgelberg Rasmus Ejlers , Zwart Maaike Annebet , Aguirre Alejandro , Birkedal Lars
Published: January 2025

Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about
FPC
⊕
, a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics of
FPC
⊕
, as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.
Generic Refinement Types
Authors: Lehmann Nico , Kurashige Cole , Akiti Nikhil , Krishnakumar Niroop , Jhala Ranjit
Published: January 2025

We present Generic Refinement Types:

a way to write modular higher-order specifications

that abstract invariants over function contracts,

while preserving automatic SMT-decidable verification.

We show how generic refinements let us write

a variety of modular higher-order specifications,

including specifications for Rust's traits

which abstract over the concrete refinements

that hold for different trait implementations.

We formalize generic refinements in a core calculus

and show how to synthesize the generic

instantiations algorithmically at usage sites via a combination of

syntactic unification and constraint solving.

We give semantics to generic refinements via the

intuition that they correspond to ghost parameters,

and we formalize this intuition via a type-preserving

translation into the polymorphic contract calculus

to establish the soundness of generic refinements.

Finally, we evaluate generic refinements by implementing

them in Flux and using it for two case studies.

First, we show how generic refinements let us write modular

specifications for Rust's vector indexing API

that lets us statically verify the bounds safety of

a variety of vector-manipulating benchmarks from

the literature.

Second, we use generic refinements

to refine Rust's Diesel ORM library to track the

semantics of the database queries issued by client

applications, and hence, statically enforce data-dependent

access-control policies in several database-backed

web applications.
Derivative-Guided Symbolic Execution
Authors: Yuan Yongwei , Zhou Zhe , Belyakova Julia , Jagannathan Suresh
Published: January 2025

We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in
Linear Temporal Logic over Finite Traces
(LTL

f

), interpreting them as
symbolic finite automata
(SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of
symbolic derivatives
, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
Authors: Heim Philippe , Dimitrova Rayna
Published: January 2025

Infinite-state reactive synthesis has attracted significant attention in recent years, which has led to the emergence of novel symbolic techniques for solving infinite-state games.

Temporal logics featuring variables over infinite domains offer an expressive high-level specification language for infinite-state reactive systems.

Currently, the only way to translate these temporal logics into symbolic games is by naively encoding the specification to use techniques designed for the Boolean case.

An inherent limitation of this approach is that it results in games in which the semantic structure of the temporal and first-order constraints present in the formula is lost.

There is a clear need for techniques that leverage this information in the translation process to speed up solving the generated games.

In this work, we propose the first approach that addresses this gap.

Our technique constructs a monitor incorporating first-order and temporal reasoning at the formula level, enriching the constructed game with semantic information that leads to more efficient solving. We demonstrate that thanks to this, our method outperforms the state-of-the-art techniques across a range of benchmarks.
Coinductive Proofs for Temporal Hyperliveness
Authors: Correnson Arthur , Finkbeiner Bernd
Published: January 2025

Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem for such logics has been widely studied, there is a scarcity of deductive proof systems for temporal hyperproperties. In particular, hyperproperties with an alternation of universal and existential quantification over system executions are rarely supported. In this paper, we focus on hyperproperties of the form ∀
*
∃
*
ψ, where ψ is a safety relation. We show that hyperproperties of this class – which includes many hyperliveness properties of interest – can always be approximated by coinductive relations. This enables intuitive proofs by coinduction. Based on this observation, we define HyCo (
Hy
perproperties,
Co
inductively), a mechanized framework to reason about temporal hyperproperties within the Coq proof assistant. We detail the construction of HyCo, provide a proof of its soundness, and exemplify its use by applying it to the verification of reactive systems modeled as imperative programs with nondeterminism and I/O.
Interaction Equivalence
Authors: Accattoli Beniamino , Lancelot Adrienne , Manzonetto Giulio , Vanoni Gabriele
Published: January 2025

Contextual equivalence is the
de facto
standard notion of program equivalence. A key theorem is that contextual equivalence is an
equational theory
. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does
not
induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.

In the paradigmatic case of the untyped λ-calculus, we introduce
interaction equivalence
. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as ℬ, the well-known theory induced by Böhm tree equality. It is the first observational characterization of ℬ obtained
without
enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Authors: van Brügge Jan , McKinna James , Popescu Andrei , Traytel Dmitriy
Published: January 2025

This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as 𝜆-calculi and logics. It provides a general criterion that targets inductively defined rule-based systems, enabling for them inductive proofs that leverage Barendregt's variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster–Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
Authors: Verscht Lena , Kaminski Benjamin Lucien
Published: January 2025

We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers à la Dijkstra and through the lens of Kleene algebra with top and tests (TopKAT). Our main goal is to give an overview – a taxonomy – of how these program logics relate, in particular under different assumptions like for example program termination, determinism, and reversibility. As a byproduct, we obtain a TopKAT characterization of Lisbon logic, which – to the best of our knowledge – is a novel result.
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
Authors: Kim Yoonseung , Lee Sung-Hwan , Kim Yonghyun , Hur Chung-Kil
Published: January 2025

Safety-critical systems are often designed as real-time distributed systems. Despite the need for strong guarantees of safety and reliability in these systems, applying formal verification methods to real-time distributed systems at the implementation level has faced significant technical challenges.

In this paper, we present VeriRT, an end-to-end formal verification framework that closes the formal gap between high-level abstract timed specifications and low-level implementations for real-time distributed systems. Within the framework, we establish a theoretical foundation for constructing formal timed operational semantics by integrating conventional operational semantics and low-level timing assumptions, along with principles for reasoning about their timed behaviors against abstract specifications. We leverage CompCert’s correctness proofs to guarantee the correctness of the assembly implementation of real-time distributed systems. We provide two case studies on realistic real-time systems. All the results are formalized in Coq.
Sound and Complete Proof Rules for Probabilistic Termination
Authors: Majumdar Rupak , Sathiyanarayana V.R.
Published: January 2025

Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete probabilistic choice and demonic bounded nondeterminism. The qualitative question asks if the program terminates almost-surely, no matter how nondeterminism is resolved. The quantitative question asks for a bound on the probability of termination. Despite a long and rich literature on the topic, no sound and relatively complete proof systems were known for these problems. In this paper, we provide sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use variant functions as measures of distances to termination as well as supermartingales that restrain the growth of these variants almost-surely. Our completeness result shows how to construct suitable supermartingale and variant functions from an almost-surely terminating program. We also show that proofs of termination in many existing proof systems can be transformed to proofs in our system, pointing to its applicability in practice. As an application of our proof rule, we show an explicit proof of almost-sure termination for the two-dimensional random walker.
An Incremental Algorithm for Algebraic Program Analysis
Authors: Zhou Chenyu , Fang Yuzhou , Wang Jingbo , Wang Chao
Published: January 2025

We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that consists of two distinct steps: computing a path expression that succinctly summarizes the set of program paths of interest, and interpreting the path expression using a properly-defined semantic algebra to obtain program properties of interest. In this context, the goal of an incremental algorithm is to reduce the analysis time by leveraging the intermediate results computed before the program changes. We have made two main contributions. First, we propose a data structure for efficiently representing path expression as a tree together with a tree-based interpreting method. Second, we propose techniques for efficiently updating the program properties in response to changes of the path expression. We have implemented our method and evaluated it on thirteen Java applications from the DaCapo benchmark suite. The experimental results show that both our method for incrementally computing path expression and our method for incrementally interpreting path expression are effective in speeding up the analysis. Compared to the baseline APA and two state-of-the-art APA methods, the speedup of our method ranges from 160X to 4761X depending on the types of program analyses performed.