26 papers
This paper presents the first large-scale empirical study of floating-point arithmetic usage in statically typed languages across millions of GitHub repositories, revealing that while existing benchmarks are partially representative, they do not fully capture real-world code patterns, and releasing a dataset of 10 million extracted functions to guide future reasoning techniques.
This paper establishes an equivalence between right actegories with hom-objects and right-enriched categories with copowers over non-closed, non-symmetric monoidal bases, a generalization motivated by the need to support higher-order process passing in the concurrent language CaMPL.
This paper formalizes the concept of idempotent backward slices and presents a sound, efficient algorithm for extracting them from Gated Static Single Assignment (GSA) form to enable a novel sparse code-size reduction optimization that merges non-contiguous instructions, achieving up to 7.24% size reduction in specific benchmarks.
This paper introduces Arbiter, a framework that combines formal rules with multi-model LLM analysis to detect interference patterns in coding agent system prompts, revealing that prompt architecture influences failure types and that multi-model evaluation uncovers distinct vulnerabilities missed by single-model approaches.
This paper introduces **Turn**, a compiled, actor-based programming language that enhances agentic software by integrating LLM inference as a typed primitive with schema validation, confidence-based control flow, isolated actor contexts, capability-based identity, and compile-time schema absorption to enforce critical safety and state invariants at the language level.
This paper addresses the limitation of existing creative activity tracing methods that capture state changes without preserving intent or higher-level structure by proposing three complementary domain-specific approaches: a node-based interface for GenAI, a vocabulary of visual cues for visualization authoring, and a semantic history-embedded programming model.
This paper proposes a novel approach to mining data-aware temporal specifications from execution traces by combining Syntax Guided Synthesis with a finite-prefix interpretation of Temporal Stream Logic (TSL), enabling the robust and sample-efficient synthesis of reactive programs that capture both data transformations and temporal behaviors.
This paper presents PolyBlocks, a modular, MLIR-based compiler infrastructure that utilizes pass pipelines and analytical cost models to automatically generate high-performance code for AI chips, demonstrating competitive or superior performance against existing frameworks like Torch Inductor and XLA on NVIDIA GPUs.
EAGLE-Pangu is a reproducible system that adapts EAGLE-3-style tree speculative decoding for Ascend NPUs with Pangu teacher models by introducing an explicit cache manager, accelerator-safe tensorization, and a fused-kernel verification path, achieving up to 2.46x throughput improvement over greedy decoding.
This paper introduces vLLM Hook, an open-source plug-in that enables the programmable access and manipulation of internal model states within the vLLM inference engine to support advanced test-time alignment techniques such as adversarial prompt detection, enhanced RAG, and activation steering.
This paper develops a higher-order abstract GSOS framework that represents operational semantics via pointed higher-order GSOS laws, thereby establishing general compositionality results for higher-order languages like the SKI and -calculi.
This paper introduces a fully symbolic compiler analysis that derives cache locality as polynomials for affine loop nests, achieving 99.6% accuracy in predicting data movement across 41 scientific kernels with negligible prediction time after an average 41-second derivation.
This paper introduces VyZX, a verified library and IDE-integrated visualizer that enables formal reasoning about inductively defined graphical languages, specifically demonstrating its application to prove the soundness of the ZX-calculus for quantum computation.
This paper presents ZipLex, a formally verified framework in Scala that achieves linear-time invertible lexical analysis with longest-match semantics by combining a novel token sequence abstraction with verified data structures like zippers and memoization, demonstrating performance comparable to unverified tools while providing rigorous proofs of correctness and invertibility.
This paper introduces "Linear Layouts," a novel framework that models tensor layouts as linear algebra operations over to enable generic, efficient, and bug-free layout definitions and conversions for deep learning workloads, successfully integrating with the Triton compiler to overcome the limitations of existing case-by-case approaches.
This paper proposes a lightweight, amortized technique for selecting a subset of type annotations based on data flow to mitigate performance degradation in gradually typed programs, achieving comparable execution speed to existing methods while significantly reducing compilation time.
This paper presents an improved, modular version of the JoinActors library for Scala 3 that leverages metaprogramming to provide a developer-friendly API and an extensible architecture for integrating, comparing, and optimizing various join pattern matching algorithms, demonstrating significant performance gains over previous implementations while maintaining semantic correctness.
This paper evaluates nine state-of-the-art Large Language Models on three new benchmarks (CodeGen, Repair, and Explain) within an OCaml functional programming course, revealing that while top models effectively handle syntax/type corrections and conceptual questions, they solve significantly fewer homework problems in this low-resource language compared to high-resource languages like Python and Java.
This paper identifies and categorizes the specific pitfalls encountered when porting virtual machines to the CHERI architecture, highlighting how common C language assumptions and VM implementation idioms conflict with CHERI's strict memory safety model, and proposes verified workarounds through a case study of porting CRuby.
This paper proposes "Hybrid Structured Editing," a novel approach that bridges the gap between tool builders and users by enforcing structural constraints on code to ensure reliable tool integration while simultaneously providing programmers with a familiar and consistent text-based editing interface.