iiinova — where your digital self keeps evolving

arxiv cs.PL @arxiv-cs-pl.bsky.social · 01/10/2026

Ishan K Singavarapu, Manish Bhatt A Trust Ledger and an Execution Check for CPG-Based C-to-Lean 4 Autoformalization: Separating Declined from Silently Incorrect Translations arxiv.org/abs/2609.38237

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 01/10/2026

Eric Allen A Calculus for Units of Measure with Conversion arxiv.org/abs/2609.38242

010

arxiv cs.PL @arxiv-cs-pl.bsky.social · 01/10/2026

Fernando Lucatelli Nunes Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion) arxiv.org/abs/2609.40046

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 01/10/2026

Haokun Li, Zhongyi Wang, Guanyan Li, Xiao Yi, Shengchao Qin, Jianwei Yin, Mingshuai Chen Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements arxiv.org/abs/2609.40119

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 28/09/2026

Karuna Grewal, P. Brighten Godfrey, Justin Hsu SafeNom: Data-Aware Microservice Policies arxiv.org/abs/2609.30394

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 28/09/2026

Akash Gaonkar, Mike He, Yi Li, Bo-Yuan Huang, Andrew Cheung, Vishal Canumalla, Gus Henry Smith, Zachary Tatlock, Grigory Fedyukovich, Sharad Malik, Aarti Gupta Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators arxiv.org/abs/2609.30651

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Seyed Armin Vakil Ghahani, Manos Kapritsos Synthesizing Proofs Using Proof Sharding and Exploration arxiv.org/abs/2609.28535

010

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Serafima Nerush, Eitan Frachtenberg Pack Iteration in Swift: Ordinary Control Flow for Variadic Generics arxiv.org/abs/2609.28822

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Heru Wang, Wei Li, Zhenyu Bai, Tulika Mitra Schedules Are Solvable Symbols: Tuning-Free Compilation of Tile Programs on Dataflow Architectures arxiv.org/abs/2609.29219

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Lihan Xie, Zhicheng Hui, Yingjun Lan, Zhehao Li, Xingzhi Qi, Siyue Huang, Jirui Liu, Chuxiao Zeng, Bohan Zhao, Qinxiang Cao ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions arxiv.org/abs/2609.29296

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Pierre Goutagny, Aymeric Fromherz, Rapha\"el Monat DueList: A Theory of Lists with Combinators for SMT Solvers arxiv.org/abs/2609.29962

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Robbe De Greef, Th\'eo Engels, Felix Van den Broucke, Ken Hasselmann, Antonio Paolillo Lifting the Preprocessor with Oxidize: Structure-Preserving C-to-Rust Translation (Technical Report) arxiv.org/abs/2609.30062

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/09/2026

Chik\'e Abuah Forte: A sensitivity type system for imperative Rust arxiv.org/abs/2609.30254

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 23/09/2026

Yifeng He, Jiachen Liu Beyond Natural Language: An Agent-Native Language for Autonomous Science arxiv.org/abs/2609.25421

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 23/09/2026

Ramy Shahin Modular Composition of Inductive Types Using Lean Meta-programming arxiv.org/abs/2609.25427

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 17/09/2026

Ali Ataollahi, Fatemeh Ghassemi, Eduard Kamburjan, Marjan Sirjani Behavioral Analysis of Timed Actors using Syntactic Slice Equivalence arxiv.org/abs/2609.17840

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 17/09/2026

Qunhui Zhang MSLL: A Runtime Multi-Stack Parsing Approach for Interactive Grammar Development - A Lightweight Extension of LL-Style Recursive Descent arxiv.org/abs/2609.19063

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 15/09/2026

Catalin Toma, Manuel Oriol Modeling Quantum Computing with $\pi$-calculus arxiv.org/abs/2609.13156

010

arxiv cs.PL @arxiv-cs-pl.bsky.social · 15/09/2026

Shengyi Wang, Kathrin Stark, Andrew W. Appel Verification of a Generational Garbage Collector arxiv.org/abs/2609.13186

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 15/09/2026

Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi Equality saturation theory exploration `a la carte arxiv.org/abs/2609.14527

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 15/09/2026

Jacob Malloy, Michael R. Jantz, Terry Jones Opportunistic ZGC: Leveraging Idle Cores for More Effective Concurrent Garbage Collection arxiv.org/abs/2609.15558

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/09/2026

Nicklas Nidh\"ogg Certified Panic Mode: Repair-Invariant Error Recovery for Maximal-Munch Lexing arxiv.org/abs/2609.10600

011

arxiv cs.PL @arxiv-cs-pl.bsky.social · 04/09/2026

Gaurav Verma, Michael Canesche, Fernando Magno Quint\~ao Pereira Enhancing the Power of Polyhedral-Based Optimizations with Coordinate-Based Hill Climbing arxiv.org/abs/2609.03114

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 04/09/2026

Guanxuan Wu, Allison Sullivan Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study arxiv.org/abs/2609.03998

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 28/08/2026

Parker Ziegler, David Minh-Duy Cao, Justin Lubin, Sarah E. Chasins Direct Manipulation and Natural Language Programming, Together at Last? arxiv.org/abs/2608.26359

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 28/08/2026

Vincent Wang-Ma\'{s}cianica You may implement this later: Cofunctors as partial implementations arxiv.org/abs/2608.27180

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 28/08/2026

Chik\'e Abuah Tacet: A Language and Type System for Automatic Statistical Validity Accounting arxiv.org/abs/2608.27451

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 27/08/2026

Yifan Shi (Peking University, DeepSeek-AI), Wei Zhang (Peking University), Tianyi Cui (DeepSeek-AI) A Programming Paradigm for Spatiotemporal Composability arxiv.org/abs/2608.25512

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Hiroyuki Nakahata SAGA: A Comparison Theorem for Local-to-Global Software Architecture - From Semantic Repair Cohomology to Algebraic-Geometric Descent arxiv.org/abs/2608.21458

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Clemens Eisenhofer, Yuwen Jia, Daniel Kroening, Sergey Pupyrev Tensor Seeks Layout: Formalizing Layout Selection for ML Compilers arxiv.org/abs/2608.21555

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Md Zarzees Uddin Shah Chowdhury, Rabib Jahin Ibn Momin, Rifat Shahriyar Rust for Secure Backend Development: A Critical Review and Extended Vulnerability Comparison with Node.js and Django arxiv.org/abs/2608.22624

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Tina Massoudi, Chris Dutchyn VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education arxiv.org/abs/2608.22630

010

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Yusheng Zheng, Xiaoyu Song, Yanpeng Hu, Lebin Cheng, Yuxi Huang, Wei Zhang When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits arxiv.org/abs/2608.22928

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Simon Daniel, Timon B\"ohler, David Richter, Pascal Weisenburger, Mira Mezini On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values arxiv.org/abs/2608.23237

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 25/08/2026

Matthew Keenan, Nishant Kheterpal, Jean-Baptiste Jeannin, Cyrus Omar Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction arxiv.org/abs/2608.23309

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 20/08/2026

Sayed Mahbub Hasan Amiri, Atiar Zahan MicroPython and CircuitPython: Pythons Quiet Takeover of IoT and Robotics arxiv.org/abs/2608.18160

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 20/08/2026

Dinghong Zhong, Alexander Bai, Mikail Khan, Guannan Wei Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version) arxiv.org/abs/2608.18327

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 20/08/2026

Emma Ahrens, Samuel Rode, Philipp Schr\"oer, Joost-Pieter Katoen Towards a Deductive Verification Infrastructure for Weighted Programming arxiv.org/abs/2608.18971

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 18/08/2026

Andrew Laramore, Joseph Spracklen, Murtuza Jadliwala Beyond Single-Vulnerability Evaluation: Closing the Engineering Decision Gap Between C Retrofits and Native Safety arxiv.org/abs/2608.15486

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 18/08/2026

Katherine Wu, Jules Jacobs, Kevin Batz, Alexandra Silva Type-Directed Discretization of Probabilistic Programs (Extended Version) arxiv.org/abs/2608.16093

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 18/08/2026

Timon B\"ohler, Simon Daniel, David Richter, Pascal Weisenburger, Mira Mezini Mechanizing Choreographic Programs and Hoare Logic with State Transformers arxiv.org/abs/2608.16346

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 14/08/2026

Bernd Finkbeiner, Martin Fr\"anzle, Florian Kohn, Paul Kr\"oger Stream-based Online and Offline Monitoring under Measurement Noise arxiv.org/abs/2608.13211

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 14/08/2026

Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen Multiobjective Preexpectation Reasoning for Probabilistic Programs arxiv.org/abs/2608.13268

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 14/08/2026

Samuel Frontull, Manuel Meitinger, Georg Moser Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version) arxiv.org/abs/2608.11833

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/08/2026

Shabnam Ghasemirad, Christoph Sprenger, Si Liu, David Basin Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions arxiv.org/abs/2608.07793

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/08/2026

Yuito Murase, Atsushi Igarashi Refined^2 Environment Classifiers arxiv.org/abs/2608.07888

001

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/08/2026

Huiling Wu, Yuxin Deng ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation arxiv.org/abs/2608.07973

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/08/2026

Ye Xiong, Xiangyu Gao, Qiaochu Chen, Mingyu Li, Haibo Chen SimP: Unifying Syntax- and Semantic-Guided Techniques for Efficient Program Reduction arxiv.org/abs/2608.08352

000

arxiv cs.PL @arxiv-cs-pl.bsky.social · 11/08/2026

Xiaoquan Xu, Chenke Liu, Boning Meng, Zihao Shen, Li Zhou Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits arxiv.org/abs/2608.08765

000