New on arXiv
Sort: by field | by arXiv number | trending
Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation
Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees that programs without borrow errors inherently could not access invalid references (i.e., pointers). However, existing work on formalizing borrow checking treats it either as a component of type systems or as symbolic...
TauLang: A Language and Compiler for Space-Time Programming on Statically Scheduled Accelerators
Statically scheduled accelerators such as Groq's Tensor Streaming Processor (TSP) achieve low-latency large language model inference by stripping dynamic synchronization hardware from the chip. With no caches, arbiters, or hardware schedulers, the compiler must fix the exact slice and issue cycle of every operation, so when an operation runs is a condition for correctness. Existing kernel...
Demystifying Information Flow Downgrading using the Real--Ideal Paradigm
The real--ideal paradigm, an approach to security specification developed in the cryptography community, has the benefit that it can express sophisticated confidentiality and integrity requirements, even for decentralized systems. We show that this paradigm is the basis for a powerful and intuitive new semantic framework for language-based security. Our new framework cleanly and extensionally...
Only titles, authors and the start of each abstract are shown here, as arXiv published them. Open a paper to read its whole abstract and, with your own AI key, a plain-language summary. Papers on arXiv are preprints and may not have been peer reviewed.
Data from arXiv, used through the arXiv API. Thank you to arXiv for use of its open access interoperability.