Why we think this paper is great for you:
This paper delves into advanced concepts within functional programming, exploring how linearity can be understood semantically in non-strict evaluation contexts. It directly addresses core aspects of language design relevant to your interests.

Abstract
Traditionally, in linearly typed languages, consuming a linear resource is synonymous with its syntactic occurrence in the program. However, under the lens of non-strict evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is executed. While this distinction has been largely unexplored, it turns out to be inescapable in Haskell's optimising compiler, which heavily rewrites the source program in ways that break syntactic linearity but preserve the program's semantics. We introduce Linear Core, a novel system which accepts the lazy semantics of linearity statically and is suitable for lazy languages such as the Core intermediate language of the Glasgow Haskell Compiler. We prove that Linear Core is sound, guaranteeing linear resource usage, and that multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base.

AI Summary

• Linear Core introduces a novel type system for lazy functional languages like GHC Core that correctly accounts for the lazy semantics of linearity, distinguishing it from traditional syntactic linearity. [3]
• Linear Core: A novel pure linear calculus (λπΔ) designed for lazy languages like GHC Core, combining linearity-in-the-arrow and multiplicity polymorphism with features like algebraic datatypes, case expressions, and recursive lazy let bindings, specifically designed to accept the lazy semantics of linearity. [3]
• Lazy semantics of linearity: An understanding of linearity where a syntactic occurrence of a resource does not necessarily entail its use during program execution, contrasting with traditional syntactic linearity, and exposed by non-strict evaluation. [3]
• The system is proven sound, guaranteeing linear resource usage even under non-strict evaluation, and validates multiple optimising transformations that would otherwise break linearity in Core. [2]
• Linear Core achieves its goals through a unique combination of features: explicit tracking of captured linear resources via usage environments, distinct treatment of case scrutinees based on their Weak Head Normal Form (WHNF) status, and the introduction of irrelevant and tagged resources for fine-grained control over variable usage. [2]
• The paper provides a precise semantic definition of linearity through an instrumented operational semantics, where programs violating linear resource usage get stuck, thus formalizing the lazy semantics of linearity. [2]
• The system accepts a vast majority of semantically linear programs and optimising transformations that are rejected by traditional linear typing disciplines due to their inability to account for non-strict evaluation. [2]
• Usage environments (Δ): A fundamental construct in Linear Core that annotates Δ-bound variables, encoding the idea that lazy variable bindings consume resources only when the bound variables themselves are consumed, and ensuring mutual exclusivity between using the binder and its captured resources. [2]
• Δ-bound variables: Variables annotated with a usage environment Δ, where using such a variable is equivalent to consuming all linear resources in its annotated Δ, and mutually exclusive with directly using those Δ resources. [2]
• The implementation of Linear Core as a GHC compiler plugin demonstrates its practical applicability, successfully accepting programs resulting from transformations in linearity-heavy libraries such as `linear-base`. [1]

Why we think this paper is great for you:
This paper introduces a new programming language specifically designed for spatial dataflow architectures, which aligns well with your interest in programming language design and novel paradigms. It explores how to program specialized hardware effectively.

Abstract
Spatial dataflow architectures like the Cerebras Wafer-Scale Engine achieve exceptional performance in AI and scientific applications by leveraging distributed memory across processing elements (PEs) and localized computation. However, programming these architectures remains challenging due to the need for explicit orchestration of data movement through reconfigurable networks-on-chip and asynchronous computation triggered by data arrival. Existing FPGA and CGRA programming models emphasize loop scheduling but overlook the unique capabilities of spatial dataflow architectures, particularly efficient dataflow over regular grids and intricate routing management. We present SPADA, a programming language that provides precise control over data placement, dataflow patterns, and asynchronous operations while abstracting architecture-specific low-level details. We introduce a rigorous dataflow semantics framework for SPADA that defines routing correctness, data races, and deadlocks. Additionally, we design and implement a compiler targeting Cerebras CSL with multi-level lowering. SPADA serves as both a high-level programming interface and an intermediate representation for domain-specific languages (DSLs), which we demonstrate with the GT4Py stencil DSL. SPADA enables developers to express complex parallel patterns -- including pipelined reductions and multi-dimensional stencils -- in 6--8x less code than CSL with near-ideal weak scaling across three orders of magnitude. By unifying programming for spatial dataflow architectures under a single model, SPADA advances both the theoretical foundations and practical usability of these emerging high-performance computing platforms.

Why we think this paper is great for you:
This paper explores methods for generating well-structured, maintainable code at the class level, which is highly relevant to your interest in object-oriented programming and design patterns. It investigates how to achieve better software architecture through automated generation.

Abstract
Modern software systems require code that is not only functional but also maintainable and well-structured. Although Large Language Models (LLMs) are increasingly used to automate software development, most studies focus on isolated, single-agent function-level generation. This work examines how process structure and role specialization shape multi-agent LLM workflows for class-level code generation. We simulate a Waterfall-style development cycle covering Requirement, Design, Implementation, and Testing using three LLMs (GPT-4o-mini, DeepSeek-Chat, and Claude-3.5-Haiku) on 100 Python tasks from the ClassEval benchmark. Our findings show that multi-agent workflows reorganize, rather than consistently enhance, model performance. Waterfall-style collaboration produces cleaner and more maintainable code but often reduces functional correctness (-37.8\% for GPT-4o-mini and -39.8\% for DeepSeek-Chat), with Claude-3.5-Haiku as a notable exception (+9.5\%). Importantly, process constraints shift failure characteristics: structural issues such as missing code decrease, while semantic and validation errors become more frequent. Among all stages, Testing exerts the strongest influence by improving verification coverage but also introducing new reasoning failures, whereas Requirement and Design have comparatively modest effects. Overall, this study provides empirical evidence that software process structure fundamentally alters how LLMs reason, collaborate, and fail, revealing inherent trade-offs between rigid workflow discipline and flexible problem-solving in multi-agent code generation.

Why we think this paper is great for you:
This paper explores a novel approach to programming cryptographic proofs, which might offer insights into specialized programming paradigms or structural design principles in a unique domain. You might find the concept of 'structural duality' intriguing from a design perspective.

Abstract
Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world applications optimize predicate definitions to minimize proof generation overhead, but must correspondingly transform predicate inputs. Implementing these two steps separately duplicates logic that must precisely match to avoid catastrophic security flaws. We address this shortcoming with zkStruDul, a language that unifies input transformations and predicate definitions into a single combined abstraction from which a compiler can project both procedures, eliminating duplicate code and problematic mismatches. zkStruDul provides a high-level abstraction to layer on top of existing NIZK technology and supports important features like recursive proofs. We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.

Why we think this paper is great for you:
This paper discusses modeling layout abstractions within deep learning compilers, which touches upon the underlying design principles and implementation challenges in managing data structures. It offers a perspective on how complex mappings are handled in system design.

Abstract
Modern deep learning compilers rely on layout abstractions to manage the complex mapping between logical tensor structures and physical memory arrangements. CuTe layouts and Triton linear layouts are widely adopted industry standards. However, these layout systems operate independently with distinct mathematical underpinnings, preventing unified formal analysis and cross-system reasoning. We bridge this gap by introducing a novel approach that leverages the Integer Set Library (ISL) to create a unified mathematical representation for both layout systems through integer set relations, thereby enabling rigorous formal analysis, correctness verification, and the foundation for future cross-system optimization strategies. Our approach models CuTe layouts through integer set relations that encode the transformation from multi-dimensional coordinates to linear indices using stride-based calculations, including sophisticated swizzle operations that perform bit-level manipulations for enhanced memory access patterns. For Triton linear layouts, we construct integer set relations that model the binary vector space transformations where arithmetic operations follow finite field F_2 rules. We implement a complete suite of layout manipulation algorithms for composition, inversion, complement using built-in operations in ISL to ensure mathematical correctness and preserve layout semantics. Experimental evaluation shows that the system handles the full spectrum of layout complexity, from elementary identity transformations to sophisticated multi-dimensional tensor arrangements with complex stride configurations and swizzle patterns, validating the mathematical modeling approach across different layout paradigms.

Why we think this paper is great for you:
This paper investigates the theoretical aspects of language generation, which can inform your understanding of how formal languages are constructed and evolve. It explores the fundamental challenges in creating new language elements.

Abstract
We study language generation in the limit, where an algorithm observes an adversarial enumeration of strings from an unknown target language $K$ and must eventually generate new, unseen strings from $K$. Kleinberg and Mullainathan [KM24] proved that generation is achievable in surprisingly general settings. But their generator suffers from ``mode collapse,'' producing from an ever-smaller subset of the target. To address this, Kleinberg and Wei [KW25] require the generator's output to be ``dense'' in the target language. They showed that generation with density, surprisingly, remains achievable at the same generality. Both results assume perfect data: no noisy insertions and no omissions. This raises a central question: how much contamination can generation tolerate? Recent works made partial progress on this question by studying (non-dense) generation with either finite amounts of noise (but no omissions) or omissions (but no noise). We characterize robustness under contaminated enumerations: 1. Generation under Contamination: Language generation in the limit is achievable for all countable collections iff the fraction of contaminated examples converges to zero. When this fails, we characterize which collections are generable. 2. Dense Generation under Contamination: Dense generation is strictly less robust to contamination than generation. As a byproduct, we resolve an open question of Raman and Raman [ICML25] by showing that generation is possible with only membership oracle access under finitely many contaminated examples. Finally, we introduce a beyond-worst-case model inspired by curriculum learning and prove that dense generation is achievable even with infinite contamination provided the fraction of contaminated examples converges to zero. This suggests curriculum learning may be crucial for learning from noisy web data.

Why we think this paper is great for you:
While focused on large language models, this paper explores optimization techniques for structured reasoning processes. It might offer a different perspective on how complex logical steps can be optimized.

Abstract
Training Large Language Models (LLMs) for chain-of-thought reasoning presents a significant challenge: supervised fine-tuning on a single "golden" rationale hurts generalization as it penalizes equally valid alternatives, whereas reinforcement learning with verifiable rewards struggles with credit assignment and prohibitive computational cost. To tackle these limitations, we introduce InTRO (In-Token Rationality Optimization), a new framework that enables both token-level exploration and self-feedback for accurate and concise reasoning. Instead of directly optimizing an intractable objective over all valid reasoning paths, InTRO leverages correction factors-token-wise importance weights estimated by the information discrepancy between the generative policy and its answer-conditioned counterpart, for informative next token selection. This approach allows the model to perform token-level exploration and receive self-generated feedback within a single forward pass, ultimately encouraging accurate and concise rationales. Across six math-reasoning benchmarks, InTRO consistently outperforms other baselines, raising solution accuracy by up to 20% relative to the base model. Its chains of thought are also notably more concise, exhibiting reduced verbosity. Beyond this, InTRO enables cross-domain transfer, successfully adapting to out-of-domain reasoning tasks that extend beyond the realm of mathematics, demonstrating robust generalization.