cs.PL Arbeiten | Gist.Science

Actegories, Copowers, and Higher-Order Message Passing Semantics

Dieser Artikel erweitert die Äquivalenz zwischen rechten Aktoritäten mit Hom-Objekten und rechten, mit Kopotenzen ausgestatteten, angereicherten Kategorien auf nicht-kommutative und nicht-abgeschlossene monoidale Basen, um die Semantik höherordniger Nachrichtenübermittlung in der concurrenten Sprache CaMPL zu ermöglichen, bei der Prozesse als sequenzielle Daten weitergegeben werden müssen, um die lineare Einschränkung der Duplizierung von Ressourcen zu umgehen.

Robin Cockett (University of Calgary), Melika Norouzbeygi (University of Calgary)Wed, 11 Ma💻 cs

Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages

Diese Studie analysiert erstmals in großem Maßstab die Verwendung von Gleitkommaarithmetik in öffentlich zugänglichen GitHub-Repositories statisch typisierter Sprachen, um durch die Veröffentlichung eines Datensatzes mit 10 Millionen Funktionen und den Vergleich mit bestehenden Benchmarks die Lücke zwischen theoretischen Forschungsansätzen und realer Praxis zu schließen.

Andrea Gilot, Tobias Wrigstad, Eva DarulovaWed, 11 Ma💻 cs

Turn: A Language for Agentic Computation

Die Arbeit stellt Turn vor, eine kompilierte, actor-basierte Programmiersprache, die durch sprachintegrierte Konstrukte wie typsichere LLM-Inferenz, ein kapazitätsbasiertes Identitätssystem und einen isolierten Actor-Prozessmodell agente Software entwickelt, die autonom durch Large Language Models (LLMs) reasoning und Handeln kann.

Muyukani KizitoWed, 11 Ma🤖 cs.AI

Arbiter: Detecting Interference in LLM Agent System Prompts

Die Arbeit stellt Arbiter vor, ein Framework zur Erkennung von Interferenzmustern in Systemprompts von LLM-Coding-Agenten, das durch formale Regeln und Multi-Modell-Analysen bei drei großen Anbietern zahlreiche Schwachstellen aufdeckt und zeigt, dass die Prompt-Architektur die Fehlerklassen, nicht aber deren Schweregrad bestimmt.

Tony MasonWed, 11 Ma🤖 cs.AI

Idempotent Slices with Applications to Code-Size Reduction

Dieses Papier formalisiert den Begriff der idempotenten Rückwärtsschnitte, stellt einen korrekten und effizienten Algorithmus zu deren Extraktion in GSA-Form vor und demonstriert deren praktische Anwendung zur sparsamen Reduzierung des Code-Umfangs durch das Zusammenführen nicht-contiguierender Anweisungsfolgen.

Rafael Alvarenga de Azevedo, Daniel Augusto Costa de Sa, Rodrigo Caetano Rocha, Fernando Magno Quintão PereiraWed, 11 Ma💻 cs

vLLM Hook v0: A Plug-in for Programming Model Internals on vLLM

Das Paper stellt vLLM Hook vor, ein Open-Source-Plug-in für vLLM, das durch passive und aktive Programmierung den Zugriff auf interne Modellzustände ermöglicht, um Anwendungen wie die Erkennung von Prompt-Injection, die Verbesserung von RAG und das Aktivitäts-Steering zu unterstützen.

Ching-Yun Ko, Pin-Yu ChenTue, 10 Ma🤖 cs.LG

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

Diese Arbeit erweitert das Mining von Spezifikationen aus Ausführungsstraces über reine Boolesche Abstraktionen hinaus, indem sie Syntax-gesteuerte Synthese mit der temporalen Logik TSL $_f$ kombiniert, um datenbewusste Transformationen und Spezifikationen zu lernen und damit das passive Lernen von reaktiven Programmen in puncto Robustheit und Sample-Effizienz signifikant zu verbessern.

Sam Nicholas Kouteili, William Fishell, Christian Scaff, Mark Santolucito, Ruzica PiskacTue, 10 Ma💻 cs

PolyBlocks: A Compiler Infrastructure for AI Chips and Programming Frameworks

Die Arbeit stellt PolyBlocks vor, eine modulare, auf MLIR basierende Compiler-Infrastruktur, die durch passbasierte Transformationen und analytische Kostenmodelle automatisch hochoptimierten Code für KI-Frameworks und Chips generiert und dabei in Tests mit Torch Inductor sowie XLA konkurrieren kann.

Uday Bondhugula, Akshay Baviskar, Navdeep Katel, Vimal Patel, Anoop JS, Arnab DuttaTue, 10 Ma🤖 cs.LG

From State Changes to Creative Decisions: Documenting and Interpreting Traces Across Creative Domains

Die Arbeit stellt drei komplementäre Ansätze vor, um in kreativen Domänen wie GenAI, Visualisierung und Programmierung nicht nur Zustandsänderungen zu erfassen, sondern auch die dahinterliegenden kreativen Absichten und Zusammenhänge zu bewahren und interpretierbar zu machen.

Xiaohan Peng, Sotiris Piliouras, Carl Abou Saada NujaimTue, 10 Ma💻 cs

EAGLE-Pangu: Accelerator-Safe Tree Speculative Decoding on Ascend NPUs

Das Paper stellt EAGLE-Pangu vor, ein reproduzierbares System, das die baumstrukturierte spekulative Decodierung auf Ascend NPUs portiert und durch einen expliziten Cache-Manager sowie accelerator-sichere Tensor-Operationen die End-to-End-Durchsatzrate im Vergleich zur reinen Lehrmodell-Decodierung signifikant steigert.

Chang Han, Yijie Hu, Jingling LiuTue, 10 Ma🤖 cs.LG

Towards a Higher-Order Mathematical Operational Semantics

Dieser Artikel entwickelt eine Theorie abstrakter GSOS-Spezifikationen für höherstufige Sprachen, die das Bialgebra-Framework von Turi und Plotkin auf diesen Bereich überträgt und durch die Einführung von „pointed higher-order GSOS laws" allgemeine Kompositionalitätsresultate für Systeme wie den SKI-Kalkül und den λ-Kalkül liefert.

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning UrbatThu, 12 Ma🔢 math

VyZX: Formal Verification of a Graphical Quantum Language

Das Paper stellt VyZX vor, eine verifizierte Bibliothek, die es ermöglicht, die Semantik und Rewrite-Regeln des ZX-Kalküls für die Quantenberechnung unter Beibehaltung der diagrammatischen Intuition in einem Beweisassistenten formal zu verifizieren.

Adrian Lehmann, Ben Caldwell, Bhakti Shah, William Spencer, Robert RandThu, 12 Ma⚛️ quant-ph

Getting Python Types Right with RightTyper

Die Arbeit stellt RightTyper vor, einen hybriden Ansatz für Python, der durch die Kombination von Laufzeitbeobachtungen, statischer Analyse und adaptivem Sampling präzise Typannotationen mit nur etwa 27 % Laufzeit-Overhead erzeugt und dabei deutlich bessere Ergebnisse als rein statische, dynamische oder KI-basierte Methoden liefert.

Juan Altmayer Pizzorno, Emery D. BergerThu, 12 Ma💻 cs

Fully Symbolic Analysis of Loop Locality: Using Imaginary Reuse to Infer Real Performance

Diese Arbeit stellt eine vollständig symbolische Theorie der Speicherlokalität vor, die mithilfe von Compiler-Analysen für affine Schleifenverschachtelungen präzise, skalierbare Polynome zur Vorhersage von Cache-Fehlern mit 99,6 % Genauigkeit ableitet.

Yifan Zhu, Yekai Pan, Chen Ding, Yanghui WuThu, 12 Ma💻 cs

Category Theory for Programming

Diese Vorlesungsnotizen führen anhand von Anwendungen in der funktionalen Programmierung kurz in die Konzepte der initialen Algebren und Monaden der Kategorientheorie ein und bieten zahlreiche Übungsaufgaben mit Lösungen.

Benedikt Ahrens, Kobe WullaertMon, 09 Ma🔢 math

Linear Layouts: Robust Code Generation of Efficient Tensor Computation Using $\mathbb{F}_2$

Die Arbeit stellt „Linear Layouts" vor, einen neuartigen Ansatz zur effizienten Generierung von Tensor-Berechnungen, der Tensor-Layouts mithilfe linearer Algebra über $\mathbb{F}_2$ modelliert, um eine generische Definition und Konvertierung zu ermöglichen, den Engineering-Aufwand zu reduzieren und die Leistung von Triton-Operatoren zu optimieren.

Keren Zhou, Mario Lezcano, Adam Goucher, Akhmed Rakhmati, Jeff Niu, Justin Lebar, Pawel Szczerbuk, Peter Bell, Phil Tillet, Thomas Raoux, Zahi MoudallalMon, 09 Ma💻 cs

Formally Verified Linear-Time Invertible Lexing

Die Arbeit stellt ZipLex vor, ein in Stainless verifiziertes Framework für invertible lineare lexikalische Analyse, das durch den Einsatz von Zippern und verifizierter Memoisierung nicht nur die längste Übereinstimmung garantiert, sondern auch die Linearzeitkomplexität und die Umkehrbarkeit von Lexing und Printing nachweist.

Samuel Chassot, Viktor KunčakMon, 09 Ma💻 cs

Hybrid Structured Editing: Structures for Tools, Text for Users

Der Artikel stellt „Hybrid Structured Editing" vor, einen Ansatz, der Tool-Entwicklern strukturelle Garantien für die Code-Analyse bietet, während Benutzern gleichzeitig eine vertraute und konsistente Textbearbeitungsschnittstelle erhalten bleibt.

Tom Beckmann (Hasso Plattner Institute, Germany / University of Potsdam, Germany), Christoph Thiede (Hasso Plattner Institute, Germany / University of Potsdam, Germany), Jens Lincke (Hasso Plattner Institute, Germany / University of Potsdam, Germany), Robert Hirschfeld (Hasso Plattner Institute, Germany / University of Potsdam, Germany)Mon, 09 Ma💻 cs

Pitfalls in VM Implementation on CHERI: Lessons from Porting CRuby

Dieser Beitrag analysiert anhand des Portings von CRuby auf CHERI spezifische Fallstricke bei der Implementierung von Virtual Machines, die durch die Kollision von C-Programmierungsideen mit dem strengen CHERI-Sicherheitsmodell entstehen, und stellt bewährte Lösungen vor.

Hanhaotian Liu (University of Tokyo, Japan), Tetsuro Yamazaki (University of Tokyo, Japan), Tomoharu Ugawa (University of Tokyo, Japan)Mon, 09 Ma💻 cs

Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study

Diese Studie bewertet die Leistungsfähigkeit von neun fortschrittlichen Large-Language-Modellen im Kontext eines funktionalen Programmierkurses mit der Low-Resource-Sprache OCaml, indem sie drei neue Benchmarks für Codegenerierung, -korrektur und -erklärung nutzt und feststellt, dass die besten Modelle zwar effektiv sind, aber im Vergleich zu Hochressourcen-Sprachen wie Python oder Java weniger Hausaufgaben lösen können.

Yihan Zhang (McGill University, Canada), Brigitte Pientka (McGill University, Canada), Xujie Si (University of Toronto, USA)Mon, 09 Ma💻 cs

Weiter →

cs.PL