David M Kahn, Jan Hoffmann, Thomas Reps, Jessie Grosen Efficient Cost Bounds with Linear Maps https://arxiv.org/abs/2509.22982

Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification https://arxiv.org/abs/2509.23061

Yawen Guan, Cl\'ement Pit-Claudel Fine-Grained Reasoning About Container-Internal Pointers with Logical Pinning https://arxiv.org/abs/2509.23229

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, R\'emi Pr\'ebet From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry https://arxiv.org/abs/2509.25114

Anjiang Wei, Tarun Suresh, Tianran Sun, Haoze Wu, Ke Wang, Alex Aiken InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis? https://arxiv.org/abs/2509.21629

Jianhong Zhao, Everett Hildenbrandt, Juan Conejero, Yongwang Zhao Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics https://arxiv.org/abs/2509.21793

Dmitri Volkov, Yafei Yang, Chung-chieh Shan Committing to the bit: Relational programming with semiring arrays and SAT solving https://arxiv.org/abs/2509.22614

Mahmoud Samir Fayed Dual-Language General-Purpose Self-Hosted Visual Language and new Textual Programming Language for Applications https://arxiv.org/abs/2509.20426

Bowen Zhu, Aayush Sabharwal, Songchen Tan, Yingbo Ma, Alan Edelman, Christopher Rackauckas Efficient Symbolic Computation vis Hash Consing https://arxiv.org/abs/2509.20534

William J. Bowman Macro-embedding Compiler Intermediate Languages in Racket https://arxiv.org/abs/2509.19607

William J. Bowman Compilation as Multi-Language Semantics https://arxiv.org/abs/2509.19613

Maurice Wenig, Paul G. Rump, Mark Blacher, Joachim Giesen The Syntax and Semantics of einsum https://arxiv.org/abs/2509.20020

Liyi Li, Fenfen An, Federico Zahariev, Zhi Xiang Chong, Amr Sabry, Mark Gordon A Verified Compiler for Quantum Simulation https://arxiv.org/abs/2509.18583

Juxin Niu, Yuxin Du, Dan Niu, Xi Wang, Zhe Jiang, Nan Guan VerilogMonkey: Exploring Parallel Scaling for Automated Verilog Code Generation with LLMs https://arxiv.org/abs/2509.16246

Savini Kashmira, Jayanaka Dantanarayana, Thamirawaran Sathiyalogeswaran, Yichao Yuan, Nishil Talati, Krisztian Flautner, Lingjia Tang, Jason Mars GraphMend: Code Transformations for Fixing Graph Breaks in PyTorch 2 https://arxiv.org/abs/2509.16248

Parosh Aziz Abdulla, Samuel Grahn, Bengt Jonsson, Shankaranarayanan Krishna, Om Swostik Mishra Efficient Linearizability Monitoring https://arxiv.org/abs/2509.17795

Shardul Chiplunkar, Cl\'ement Pit-Claudel Automatic layout of railroad diagrams https://arxiv.org/abs/2509.15834

Wyatt Petula, Anushcka Joshi, Peggy Tu, Amrutha Somasundar, Suman Saha DeliverC: Teaching Pointers through GenAI-Powered Game-Based Learning https://arxiv.org/abs/2509.14496

Facundo Dom\'inguez, Arnaud Spiwack Refinement-Types Driven Development: A study https://arxiv.org/abs/2509.15005

Anthony Arnold, Mark Marron Catalpa: GC for a Low-Variance Software Stack https://arxiv.org/abs/2509.13429

Chester J. F. Gould, William J. Bowman Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE https://arxiv.org/abs/2509.13489

Boyu Zhang, Ping He, Tianyu Du, Xuhong Zhang, Lei Yun, Kingsum Chow, Jianwei Yin CLMTracing: Black-box User-level Watermarking for Code Language Model Tracing https://arxiv.org/abs/2509.13982

Michele Boreale (University of Florence), Luisa Collodi (University of Florence) Parallelizable Feynman-Kac Models for Universal Probabilistic Programming https://arxiv.org/abs/2509.14092

Yimin Zhang, Mario de Sousa Converting IEC 61131-3 LD into SFC Using Large Language Model: Dataset and Testing https://arxiv.org/abs/2509.12593

Shermin Khosravi, David Bremner Efficient Compilation of Algorithms into Compact Linear Programs https://arxiv.org/abs/2509.13006

Fr\'ed\'eric Fort, David Nowak, Vlad Rusu Pleasant Imperative Program Proofs with GallinaC https://arxiv.org/abs/2509.13019

Andrei Nacu (Faculty of Computer Science, Alexandru Ioan Cuza University, Ia\c{s}i), Dorel Lucanu (Faculty of Computer Science, Alexandru Ioan Cuza University, Ia\c{s}i) Navigating the Python Type Jungle https://arxiv.org/abs/2509.13022

Rapha\"el Monat Try-Mopsa: Relational Static Analysis in Your Pocket https://arxiv.org/abs/2509.13128

No\'e De Santo, Stephanie Weirich Rebound: Efficient, Expressive, and Well-Scoped Binding https://arxiv.org/abs/2509.13261

Runming Li, Yue Yao, Robert Harper Mechanizing Synthetic Tait Computability in Istari https://arxiv.org/abs/2509.11418

Kentaro Kobayashi, Yukiyoshi Kameyama Expressive Power of One-Shot Control Operators and Coroutines https://arxiv.org/abs/2509.11901

Mohit Tekriwal, John Sarracino Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs https://arxiv.org/abs/2509.09019

Paulette Koronkevich, William J. Bowman Dependent-Type-Preserving Memory Allocation https://arxiv.org/abs/2509.09059

Faruk Alpay, Taylan Alpay XML Prompting as Grammar-Constrained Interaction: Fixed-Point Semantics, Convergence Guarantees, and Human-AI Protocols https://arxiv.org/abs/2509.08182

Youjie Li, Cheng Wan, Zhiqi Lin, Hongyu Zhu, Jiacheng Yang, Ziang Song, Xinyi Di, Jiawei Wu, Huiyao Shu, Wenlei Bao, Yanghua Peng, Haibin Lin, Li-Wen Chang veScale: Consistent and Efficient Tensor Programming with Eager-Mode SPMD https://arxiv.org/abs/2509.07003

Sean Bocirnea, William J. Bowman Fast and Extensible Hybrid Embeddings with Micros https://arxiv.org/abs/2509.07551

Yichen Xu, Oliver Bra\v{c}evac, Cao Nguyen Pham, Martin Odersky What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version) https://arxiv.org/abs/2509.07609

Karl Aaron Rudkowski, Sallar Ahmadi-Pour, Rolf Drechsler Comparing Methods for the Cross-Level Verification of SystemC Peripherals with Symbolic Execution https://arxiv.org/abs/2509.05504

Lee Zheng Han, Umang Mathur Fixed Parameter Tractable Linearizability Monitoring for Stack, Queue and Anagram Agnostic Data Types https://arxiv.org/abs/2509.05586

Florian Kohn, Arthur Correnson, Jan Baumeister, Bernd Finkbeiner Pacing Types: Safe Monitoring of Asynchronous Streams https://arxiv.org/abs/2509.06724

Amir M. Ben-Amram, Samir Genaim, Jo\"el Ouaknine, James Worrell Termination Analysis of Linear-Constraint Programs https://arxiv.org/abs/2509.06752

Shihan Fang, Hongzheng Chen, Niansong Zhang, Jiajie Li, Han Meng, Adrian Liu, Zhiru Zhang Dato: A Task-Based Programming Model for Dataflow Accelerators https://arxiv.org/abs/2509.06794

Tom Lauwaerts, Maarten Steevens, Christophe Scholliers MIO: Multiverse Debugging in the Face of Input/Output -- Extended Version with Additional Appendices https://arxiv.org/abs/2509.06845

Zachary Kent, Ugur Y. Yavuz, Siddhartha Jayanti, Stephanie Balzer, Guy Blelloch Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs https://arxiv.org/abs/2509.06872

Andrea Gilot, Tobias Wrigstad, Eva Darulova A Large-Scale Study of Floating-Point Usage in Statically Typed Languages https://arxiv.org/abs/2509.04936

Steven Smyth, Daniel Busch, Moez Ben Haj Hmida, Edward A. Lee, Bernhard Steffen AI-Assisted Modeling: DSL-Driven AI Interactions https://arxiv.org/abs/2509.05160

Julien Vanegue, Jules Villard, Peter O'Hearn, Azalea Raad Non-Termination Proving: 100 Million LoC and Beyond https://arxiv.org/abs/2509.05293

Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking https://arxiv.org/abs/2509.04253

Eduard Kamburjan, Vidar Norstein Klungre, Yuanwei Qu, Rudolf Schlatte, Egor V. Kostylev, Martin Giese, Einar Broch Johnsen Semantically Reflected Programs https://arxiv.org/abs/2509.03318

Shaan Nagy, Timothy Zhou, Nadia Polikarpova, Loris D'Antoni ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models https://arxiv.org/abs/2509.00360