Graphical model editing is shifting from desktop applications to web-based tools. We analyze the characteristics of existing frameworks and, based on this analysis, we derive a set of design principles that imply low-effort generation, extensive customization possibilities, and straightforward deployment of the resulting editors. On these grounds, we introduce EMFular, a purely web-based framework for managing EMF models without any backend. The accompanying EMFular generator maps a given Ecore model (an EMF metamodel) to a ready-to-use and ready-to-customize graphical editor. EMFular editors provide 'EMF consistency', that is, they not only support standard modeling operations such as creation, inspection, navigation, editing, and undo/redo, but they also handle containment and inverse references in close alignment with EMF; they also provide interoperability with existing EMF tooling through compatible de-/serialization. A generated editor is an Angular project with designated extension points, which allows developers to customize and extend all aspects of the editor using the expressive power of Angular and its ecosystem, guided by the extension points of EMFular. We evaluate EMFular in terms of editor adequacy (available editing capabilities), adaptability (customization mechanisms and required effort), and robustness of the generation.

The GraphAlg domain-specific language for graph algorithms enables user-defined algorithms in graph databases. In this work we show how GraphAlg is built on top of the formal MATLANG language for matrix manipulation. Starting from MATLANG, we describe the extensions to MATLANG and the syntactic sugar needed to derive GraphAlg. Furthermore, we prove that any GraphAlg program can be simulated in an extension of for-MATLANG that supports simultaneous induction.

We introduce Mirage Persistent Kernel (MPK), the first compiler and runtime system that automatically transforms multi-GPU model inference into a single high-performance mega-kernel. MPK introduces an SM-level graph representation that captures data dependencies at the granularity of individual streaming multiprocessors (SMs), enabling cross-operator software pipelining, \rev{fine-grained overlap of computation and communication, and other optimizations that are infeasible under the conventional kernel-per-operator execution model}. The MPK compiler lowers tensor programs into optimized SM-level task graphs and generates fast CUDA implementations for each task, while the MPK in-kernel parallel runtime executes these tasks within a single persistent mega-kernel using decentralized scheduling across SMs. Together, these components provide end-to-end kernel fusion with minimal developer effort, while preserving the flexibility of existing programming models. Our evaluation shows that MPK significantly outperforms existing kernel-per-operator LLM serving systems, achieving up to 1.7$\times$ lower end-to-end inference latency and pushing LLM inference performance close to the limits of the underlying hardware. MPK is publicly available at this https URL.

Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its "shared XOR mutable" model is fundamentally at odds with higher-level functional programming. Reachability types offer an alternative: they enable safe sharing and escape of mutable data by tracking which resources each expression's result can reach. To track internal reachability within complex object graphs, reachability types adopt self-references that let components refer to enclosing resources from inside, just like `this` pointers in OO languages. While natural for declaratively typing escaping data, self-references complicate subtyping and furthermore type inference: variance restricts where self-references may appear, yet useful type conversions must allow them to vary in controlled ways, which in turn imposes constraints on inference. As an undesirable result, prior works require programmers to insert term-level coercions for even just avoidance -- avoiding ill-scoped names in types. With all prior works being declarative, we investigate algorithmic reachability types in this work. We introduce a refined subtyping relation that permits more flexible usages of self-references. We further develop a sound and decidable bidirectional typing algorithm, implemented and verified in Lean. The algorithm automatically avoids ill-scoped names in types, and infers qualifiers via a lightweight unification mechanism. As a step towards practical reachability programming, we show that the system is capable of tracking diverse reachability patterns without explicit coercions in complex Church-encoded datatypes.

The Release-Acquire (RA) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether any allowed program run is consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the RA semantics or its Strong (SRA) and Weak (WRA) variants. We show that verifying WRA in this setup is in O(n5 ), while verifying the RA and SRA is PSPACE complete. This both answers some fundamental questions about the complexity of these problems, but also provides insights on the expressive power of register machines as a model.