Computer Science
We establish two structural majorization relations, which we call precursors, underlying the properties of supermodularity and subadditivity on the lattice induced by majorization. These are precursors in that they immediately imply that…
The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms…
We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that…
We prove a list recovery guarantee for random low-rate linear codes over sufficiently large prime fields. For fixed dimension $d$, error fraction $\alpha$, and accuracy parameter $\varepsilon$, a random $d$-dimensional linear code $C…
Superimposed pilot (SIP) transmission improves spectral efficiency by eliminating the dedicated pilot overhead required in orthogonal pilot (OP)-based schemes. However, SIP suffers from severe pilot-data coupling, which leads to a critical…
Integrated sensing, communication, and computation (ISCC) provides a promising framework for indoor human-centric applications. In these applications, short-term human pose prediction facilitates continuous human tracking and resource…
This paper investigates a multi-user indoor integrated sensing and communication (ISAC) system operating in the terahertz (THz) band, designed for adaptive communication based on gesture recognition. Leveraging gesture tracking through an…
In radar sensing, the self-ambiguity function of the probing waveform plays a crucial role in the resolvability and detection of multiple targets. In the recent Zak-OTFS based radar literature, Gaussian pulse shaping filter has been…
High Altitude Platform Stations (HAPS) have emerged as a promising enabler for next-generation wireless networks, offering ubiquitous connectivity to ground users. Operating either in standalone mode or in integration with terrestrial…
Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using…
In distributed hypothesis testing, a central server performs hypothesis testing based on information received from distributed sensors/clients. We study a secure variant of this problem in which the central server determines the hypothesis…
This paper studies Set Shaping Theory (SST) in a database-index setting under a revised interpretation: SST is not treated as a competing hashing method, but as a structural pre processing layer that can be applied before an existing…
Fluid antenna systems (FAS) have emerged as a promising technology for next-generation wireless systems. However, practical multiuser multiple-input multiple-output FAS (MIMO-FAS) faces two inherently coupled challenges: acquiring accurate…
Pinching-antenna systems (PASS) have emerged as a promising flexible-antenna architecture capable of dynamically reconfiguring wireless channels by activating dielectric particles along waveguides. The sum rate maximization problem in…
Ultra-reliable low-latency communication (uRLLC) is a pivotal enabler for B5G/6G networks, yet it faces severe challenges from rare but critical extreme events, which are characterized by heavy tails in the delay distribution. While the…
The determination of the maximal length of maximum distance separable (MDS) codes arising from elliptic curves is a central problem in coding theory. For an elliptic curve $E$ over $\mathbb{F}_q$, let $\operatorname{MEC}(k,q)$ denote the…
Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also…
We present mstlo (mistletoe), a Rust library for high-performance online monitoring of signal temporal logic (STL), with Python bindings. The library provides: (i) a unified interface for multiple STL semantics, including Robust…
Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) pipelines. In current systems, each search branch…
We improve upon the Johnson-type bound of Hayashi and Yasunaga for insertion-deletion codes by encoding each local list into a binary constant-weight code. The resulting local list-size bound is tight for sufficiently large alphabets.…