Theory & Algorithms · Computer Science & AI
Logic in Computer Science
The newest papers in Logic in Computer Science that ReadSearch has read, newest first. Each links to its own page, with its authors, date, where it was published and the original.
168 papers, from 4 September 2026 to 5 November 2026: 168 arXiv preprints.
Get the few papers worth your time in Logic in Computer Science every morning.
Follow Logic in Computer Science and ReadSearch reads its new papers each day, then brings you the few worth reading, each with its key finding in a sentence.
Newest papers
Frustration-freeness is decidable but unprovable
The frustration-free property is valuable in quantum many-body systems, which states that its ground states simultaneously minimize all local interaction terms, even when these terms act on…Typed Knowledge over Constructive Institutions
Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established.First-Order Model Checking on Monadically Dependent Graph Classes
Monadically dependent graph classes are those in which first-order logic cannot encode all graphs.From Certified Pairs to a Certified Hub: Reasoner-Checked Crosswalks for the Information Exchange Standard
A national digital twin was conceived as an ecosystem of twins connected through mappings to a common foundation, but the roadmap that promises to confirm those mappings are valid never says what…Monadically Dependent Graph Classes Have Almost Bounded Merge-Width
A graph class $\mathcal{C}$ is monadically dependent if one cannot interpret all graphs in vertex-colored graphs from $\mathcal{C}$ using a fixed formula of first-order logic.Reasoning about Shared-Qubit Concurrency in Quantum Computing
In this paper, we develop a semantic model for the parallel execution of quantum circuits, providing a formal foundation for studying shared-qubit concurrency in quantum computing.Aero-VPA: Few-Step Flow-Matching Control over Non-Reconstructive JEPA Latents for Agile Flight on Edge Hardware
Vision-Language-Action (VLA) models generalize across tasks, but their autoregressive decoders need sequential forward passes in proportion to the action horizon, each bounded below on embedded…Sketchpad: certified exact arithmetic with a small vision-language model
Language models are accurate on most long-arithmetic problems, but their accuracy is estimated on samples and carries no guarantee for an unseen input; tool use is exact but moves the computation…ProofStudio: Five Proof Assistants in the Browser
Recent advances in AI-assisted proof automation are extending the use of proof assistants in software verification and mathematics.Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs.Iterated Narrow Networks: Turing Completeness at Width 4 on Convex Input Spaces and the Complexity of Verification
We study the iterates of a fixed ReLU network $N$ of width 4, that is, the discrete-time system $x_{k+1} = N(x_k)$ on $[0,1]^4$.Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations
Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning.TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI.The Scope Grammar of Natural-Language Rules: Counting and Enumerating Readings modulo Logical Equivalence
A rule written for people fixes its atomic conditions and connectives but leaves open how the connectives are bracketed, and each bracketing is a different logical reading that an autoformalizer…Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale
When autonomous coding agents synthesize implementation code, formal specifications, and mechanical proofs simultaneously, the software engineering hierarchy inverts: the formal specification…ProofPatch: Reviewing Lean Statements and Keeping the Reviews Valid as Formalizations Evolve
The kernel of the Lean proof assistant checks that a proof establishes its statement.DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the…VerusWeave: A Benchmark for Proof Repair in Concurrent Verus Programs
Concurrent software underpins critical infrastructure, including operating systems and databases, yet thread interactions can have bugs that bypass conventional testing.Learning Erasing Equal-Length Relational Pattern Languages in the Limit from Positive Data over Binary Alphabets
Relational pattern languages generalize Angluin's pattern languages by requiring the strings substituted for repeated occurrences of a variable to stand in a given relation, rather than to be…Automated Verification of Hamiltonian Simulation by Quantum Signal Processing
We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation.