• 00 07-17 (4) GPU Performance Portability needs Autotuning GPU Performance Portability benötigt Autotuning GPU 性能表现 便捷性需要自动调节 2505.03780v3
  • 01 07-17 Towards Formal Verification of LLM-Generated Code from Natural Language Prompts Auf dem Weg zu einer formalen Überprüfung des LLM-generierten Codes aus natürlichen Sprachprompts 争取正式核查自然语言提示法LLM产生的守则 2507.13290v1
  • 02 07-17 Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE Sichere Parsing und Serialisierung mit Separation Logic auf CBOR, CDDL und COSE angewendet 安全分解和序列化,与分离逻辑结合应用到CBOR、CDDL和COSE 2505.17335v2
  • 03 07-17 Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications Formale Überprüfung für JavaScript Reguläre Ausdrücke: eine bewährte Semantik und ihre Anwendungen JavaScript 常规表达式:经验证的语义及其应用的正式验证 2507.13091v1
  • 04 07-17 Syntax Repair as Language Intersection Syntax-Reparatur als Sprach-Intersektion 语法修理作为语言交汇处 2507.11873v2
  • 05 07-16 (3) Compiling a Q# Subset to QASM 3.0 in TypeScript via a JSON Based IR Kompilieren eines Q#-Untersatzes zu QASM 3.0 in TypeScript über eine JSON-basierte IR 在类型Script中通过基于 JSON 的 IR 计算 QASM 3. 0 的 QASM 子集 2506.23407v2
  • 06 07-16 An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report) Ein algebraischer Ansatz zur asymmetrischen Delegation und polymorphen Label-Inferenz (Technischer Bericht) 对非对称授权和多色标签诱导法采用代数法(技术报告) 2504.20432v2
  • 07 07-16 Dual-Numbers Reverse AD for Functional Array Languages Dual-Nummern Reverse AD für funktionale Array-Sprachen 功能阵列语言双倍反向反向 2507.12640v1
  • 08 07-16 Modeling Open-World Cognition as On-Demand Synthesis of Probabilistic Models Modellierung der Open-World-Kognition als On-Demand-Synthese probabilistischer Modelle 将开放世界的认知建模作为概率模型的 “ 现场合成 “ 模型 2507.12547v1
  • 09 07-16 LLM-Based Config Synthesis requires Disambiguation LLM-basierte Konfig-Synthese erfordert Disambiguation 基于 LLM 的配置合成要求差异化 2507.12443v1
  • 10 07-16 GitChameleon: Evaluating AI Code Generation Against Python Library Version Incompatibilities GitChameleon: Bewertung der KI-Code-Generation gegen Python Library Version Inkompatibilitäten GitChameleon:评估AI 与 Python 图书馆版本不兼容性 2507.12367v1
  • 11 07-16 Programming Distributed Collective Processes in the eXchange Calculus Programmierung verteilter kollektiver Prozesse im eXchange Calculus eXchange Calculus 中的程序编程分配集体进程 2401.11212v5
  • 12 07-16 Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs Nanopass-Rückübersetzung von Call-Return-Bäumen für mechanisierte sichere Compilations-Proofs 机械化安全编译证明调回回树的纳米通回转换 2503.19609v3
  • 13 07-16 Dependent Multiplicities in Dependent Linear Type Theory Abhängige Vielfältigkeit in der abhängigen Lineartyptheorie 依附线类类型理论中的依附倍数 2507.08759v2
  • 14 07-16 Optimized Execution of FreeCHR Optimierte Ausführung von FreeCHR 最优化地执行自由人权委员会 2506.14485v2
  • 15 07-16 Towards Relational Contextual Equality Saturation Auf dem Weg zu einer relationalen kontextuellen Gleichstellungssättigung 走向关系背景平等饱和 2507.11897v1
  • 16 07-16 Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers Universelle Synthese von differenzierbaren numerischen Abstrakttransformatoren 不同金枪鱼可有区别的量化数字抽象变异器通用合成 2507.11827v1
  • 17 07-15 (2) A Practical Quantum Hoare Logic with Classical Variables, I Eine praktische Quantenhoare-Logik mit klassischen Variablen, I 具有古典变量的实用量子 Hoare 逻辑,I 2412.09869v2
  • 18 07-15 Picat Through the Lens of Advent of Code Picat durch die Adventslinse des Kodex 透过法典修道院的透镜 2507.11731v1
  • 19 07-15 Quantum circuits are just a phase Quantenschaltungen sind nur eine Phase 量子电路只是一个阶段 2507.11676v1
  • 20 07-15 On the Complexity of Checking Mixed Isolation Levels for SQL Transactions Über die Komplexität der Überprüfung gemischter Isolationsebenen für SQL-Transaktionen 关于SQL交易核对混合混合隔离水平的复杂性 2505.18409v3
  • 21 07-15 The downgrading semantics of memory safety Die abwertende Semantik der Speichersicherheit 内存安全词义的降级 2507.11282v1
  • 22 07-14 (1) Stream programs are monoid homomorphisms with state Stream-Programme sind monoide Homomorphismen mit Zustand 溪流方案是单一单一的同质状态方案 2507.10799v1
  • 23 07-14 Speculative Automated Refactoring of Imperative Deep Learning Programs to Graph Execution Spekulative Automatisierte Refaktorisierung imperativer Deep Learning-Programme zur Graphen-Execution 用于图表执行的势必深深学习方案的投机性自动重组 2504.05424v3
  • 24 07-14 Orthologic Type Systems Orthologische Typsysteme 矫形类型系统 2507.10482v1
  • 25 07-14 Toolsuite for Implementing Multiagent Systems Based on Communication Protocols Toolsuite zur Implementierung von Multiagentensystemen auf Basis von Kommunikationsprotokollen 基于通信议定书的用于实施多剂系统的工具 2507.10324v1
  • 26 07-14 Rows and Capabilities as Modal Effects Zeilen und Fähigkeiten als Modale Effekte 作为模式效果的行和能力 2507.10301v1
  • 27 07-14 Formal Verification of Variational Quantum Circuits Formale Überprüfung von Variations-Quantenkreisen 变量量电路的正式核查 2507.10635v1
  • 28 07-14 ReDemon UI: Reactive Synthesis by Demonstration for Web UI ReDemon UI: Reaktive Synthese durch Demonstration für Web UI ReDemon UI: 网络 UI 演示的反活动合成 2507.10099v1
  • 29 07-14 BeePL: Correct-by-compilation kernel extensions BeePL: Richtig-nach-Sammlung Kernel-Erweiterungen BEPL: 校正式编译内核扩展 2507.09883v1
  • 30 07-13 (7) Oracular Programming: A Modular Foundation for Building LLM-Enabled Software Orakuläre Programmierung: Modulare Grundlage für den Aufbau von LLM-fähiger Software 眼镜编程:建筑LLM-Enable软件模块基金会 2502.05310v2
  • 31 07-13 Equality Saturation for Optimizing High-Level Julia IR Gleichstellungssättigung für die Optimierung von High-Level Julia IR 优化高级别Julia IR 平等饱和 2502.17075v2
  • 32 07-13 Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams Gebundenes Modell Überprüfung von RISC-V-Maschinencode mit Kontext-Frei-Sprache bestellt binären Entscheidungsdiagrammen RISC-V型机器编码与无环境-无语言有秩序二进制决定图的对RISC-V型机器编码的边界模式检查 2507.09539v1
  • 33 07-13 PHOENIX: Pauli-Based High-Level Optimization Engine for Instruction Execution on NISQ Devices PHOENIX: Pauli-basierte High-Level-Optimierungs-Engine zur Instruction Execution auf NISQ-Geräten PHOENIX: 以保利为基础的高级优化引擎,用于NISQ设备指令执行 2504.03529v5
  • 34 07-11 (5) Semantic Source Code Segmentation using Small and Large Language Models Semantische Quellcode-Segmentierung mit kleinen und großen Sprachmodellen 使用小型和大语言模式的语义源代码代码分割 2507.08992v1
  • 35 07-11 Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny Können große Sprachmodelle den Studierenden helfen, Software-Korrektur zu beweisen? Eine experimentelle Studie mit Dafny 大语言模型能帮助学生证明软件正确性吗? 与Dafny的实验研究 2506.22370v3
  • 36 07-11 Filter Equivariant Functions: A symmetric account of length-general extrapolation on lists Filter Equivariant Funktionen: Eine symmetrische Darstellung der Längen-allgemeinen Extrapolation auf Listen 过滤器等同函数 : 列表中长度一般外推法的对称账户 2507.08796v1
  • 37 07-11 CCR 2.0: High-level Reasoning for Conditional Refinements CCR 2.0: Hochrangige Begründung für bedingte Veredelungen CCR 2.0: 有条件改进的高层次理由 2507.04298v2
  • 38 07-11 Heterogeneous Dynamic Logic: Provability Modulo Program Theories Heterogene dynamische Logik: Wahrscheinlichkeit Modulo-Programm Theorien 变异动态逻辑:可变莫杜洛方案理论 2507.08581v1
  • 39 07-11 SecRef: Securely Sharing Mutable References Between Verified and Unverified Code in F SecRef: Sicheres Teilen von mutierbaren Referenzen zwischen verifiziertem und ungeprüftem Code in F SecRef:F中经核实的守则与未经核实的守则之间安全分享可窃取的参考文献 2503.00404v2
  • 40 07-11 EOLANG and $\varphi$-calculus EOLANG und $\varphi$-Berechnung EOLANG 和 美元计算法 2111.13384v6
  • 41 07-11 Abstraction Functions as Types Abstraktionsfunktionen als Typen 抽象函数类型 2502.20496v2
  • 42 07-10 (4) Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version) Denotationale Semantik der graduellen Typisierung mittels Synthetischer Domänen-Theorie (Erweiterte Version) 使用合成保护域域理论(扩展版本)逐步打字的注解性语义表达式 2411.12822v2
  • 43 07-10 QCP: A Practical Separation Logic-based C Program Verification Tool QCP: Eine praktische Trennung Logisch-basiertes C-Programm Verifikationswerkzeug QCP:基于实际隔离逻辑的C方案核查工具 2505.12878v2
  • 44 07-10 Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version) Modulare Begründung über Fehlergrenzen für gleichzeitige probabilistische Programme (Erweiterte Version) 用于同时概率程序(例外版本)的错误误界的模块原因 2503.04512v2
  • 45 07-10 On Propositional Program Equivalence (extended abstract) Über Propositionelle Programmäquivalenz (erweiterte Zusammenfassung) 提议方案等效(扩展抽象) 2507.07480v1

Article 0

Title@2025-07-17 (4): GPU Performance Portability needs Autotuning

Title: GPU Performance Portability needs Autotuning GPU Performance Portability benötigt Autotuning GPU 性能表现 便捷性需要自动调节 2505.03780v3

Authors (3): Burkhard Ringlein, Thomas Parnell, Radu Stoica

As LLMs grow in complexity, achieving state-of-the-art performance requires tight co-design across algorithms, software, and hardware. Today’s reliance on a single dominant platform limits portability, creates vendor lock-in, and raises barriers for new AI hardware. In this work, we make the case for combining just-in-time (JIT) compilation with comprehensive kernel parameter autotuning to enable portable LLM inference with state-of-the-art performance without code changes. Focusing on performance-critical LLM kernels, we demonstrate that this approach explores up to 15x more kernel parameter configurations, produces significantly more diverse code across multiple dimensions, and even outperforms vendor-optimized implementations by up to 230%, all while reducing kernel code size by 70x and eliminating manual code optimizations. Our results highlight autotuning as a promising path to unlocking model portability across GPU vendors.

随着LLMS的复杂程度不断增长,实现最先进的LLM性能要求严格地共同设计各种算法、软件和硬件。今天,对单一主导平台的依赖限制了可移动性,创建了供应商锁定,并为新的AI硬件制造了障碍。在这项工作中,我们有理由将即时(JIT)汇编与全面的内核参数自动调整结合起来,以便允许便携式LLM在不改变代码的情况下对最新性能进行推论。聚焦于性能临界的LLM内核,我们证明这一方法可以探索多达15x更多的内核参数配置,在多个维度上产生更多样化得多的代码,甚至比供应商优化执行率高出230 % , 而同时将内核代码的尺寸减少70x,并消除手动代码优化。我们的结果突出表明,自动化是释放GPU供应商模型可移植性能的一条有希望的道路。

Article 1

Title@2025-07-17 (4): Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

Title: Towards Formal Verification of LLM-Generated Code from Natural Language Prompts Auf dem Weg zu einer formalen Überprüfung des LLM-generierten Codes aus natürlichen Sprachprompts 争取正式核查自然语言提示法LLM产生的守则 2507.13290v1

Authors (7): Aaron Councilman, David Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, Vikram Adve

In the past few years LLMs have emerged as a tool that can aid programmers by taking natural language descriptions and generating code based on it. However, LLMs often generate incorrect code that users need to fix and the literature suggests users often struggle to detect these errors. In this work we seek to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the experience of using AI Code Assistants and potentially enable natural language programming for users with little or no programming knowledge. To address this challenge we propose to incorporate a formal query language that can represent a user’s intent in a formally defined but natural language-like manner that a user can confirm matches their intent. Then, using such a query we propose to verify LLM generated code to ensure it matches the user’s intent. We implement these ideas in our system, Astrogator, for the Ansible programming language which includes such a formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter which is used for the verification. On a benchmark suite of 21 code-generation tasks, our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.

过去几年来,LLMS已经成为帮助程序员的工具,通过采用自然语言描述并据此生成代码来帮助程序员。然而,LLMS经常产生用户需要修正的错误代码,文献则表明用户往往会为发现这些错误而挣扎。在这项工作中,我们力求为LLM生成的代码提供正式的正确性保证;这些保障可以改善使用AI Code助理的经验,并有可能为几乎或完全没有编程知识的用户提供自然语言编程。为了应对这一挑战,我们提议纳入一种正式的查询语言,该语言可以以正式确定但自然语言相似的方式代表用户的意图,使用户能够确认其意图。然后,利用这样的询问,我们提议核查LLM生成的代码,以确保与用户的意图相符。我们在我们的系统中实施了这些想法,Astrogator,用于Asisable编程语言,其中包括一种正式的查询语言,一种代表 ANSE 程序的行为的缩略图,以及一种用于核查的象征性翻译。在21个代码生成任务的基准套中,我们的校准者能够核实83%的案例的代码,并查明92 %的代码。

Article 2

Title@2025-07-17 (4): Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

Title: Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE Sichere Parsing und Serialisierung mit Separation Logic auf CBOR, CDDL und COSE angewendet 安全分解和序列化,与分离逻辑结合应用到CBOR、CDDL和COSE 2505.17335v2

Authors (4): Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy

Incorrect handling of security-critical data formats, particularly in low-level languages, are the root cause of many security vulnerabilities. Provably correct parsing and serialization tools that target languages like C can help. Towards this end, we present PulseParse, a library of verified parser and serializer combinators for non-malleable binary formats. Specifications and proofs in PulseParse are in separation logic, offering a more abstract and compositional interface, with full support for data validation, parsing, and serialization. PulseParse also supports a class of recursive formats – with a focus on security and handling adversarial inputs, we show how to parse such formats with only a constant amount of stack space. We use PulseParse at scale by providing the first formalization of CBOR, a recursive, binary data format standard, with growing adoption in various industrial standards. We prove that the deterministic fragment of CBOR is non-malleable and provide EverCBOR, a verified library in both C and Rust to validate, parse, and serialize CBOR objects implemented using PulseParse. Next, we provide the first formalization of CDDL, a schema definition language for CBOR. We identify well-formedness conditions on CDDL definitions that ensure that they yield unambiguous, non-malleable formats, and implement EverCDDL, a tool that checks that a CDDL definition is well-formed, and then produces verified parsers and serializers for it. To evaluate our work, we use EverCDDL to generate verified parsers and serializers for various security-critical applications. Notably, we build a formally verified implementation of COSE signing, a standard for cryptographically signed objects. We also use our toolchain to generate verified code for other standards specified in CDDL, including DICE Protection Environment, a secure boot protocol standard.

安全关键数据格式的处理不正确, 特别是低级别语言的处理不正确, 是许多安全脆弱性的根源。 PulseParse 也支持一系列循环格式, 重点是安全和处理对抗性投入。 为此, 我们展示了 PulseParse。 我们使用 PulseParse, 是一个由可核实的剖析器和连序器组合组合器组成的库, 用于不可变二进制的二进制格式。 PulmalParse 中的规格和证明符合分离逻辑, 提供了更加抽象和构成的界面, 并全力支持数据验证、 解析和连序化。 PulseParse 也支持了一组循环格式, 重点是安全和处理对抗性投入, 我们展示了如何以固定的堆叠版空间来解析这些格式。 我们使用 PulseParseParse ParsePrass 标准, 运行了一种常规的 CDLL 标准, 用于在各种工业标准中不断更新的 CDL 。 我们证明, 输入了一种标准 Dral Dral 的硬化的硬文件, 。

Article 3

Title@2025-07-17 (4): Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications

Title: Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications Formale Überprüfung für JavaScript Reguläre Ausdrücke: eine bewährte Semantik und ihre Anwendungen JavaScript 常规表达式:经验证的语义及其应用的正式验证 2507.13091v1

Authors (3): Aurèle Barrière, Victor Deng, Clément Pit-Claudel

We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting line-by-line embedding of the official ECMAScript specification of JavaScript regular expressions. We demonstrate its practicality by presenting two real-world applications. First, a new notion of contextual equivalence for modern regular expressions, which we use to prove or disprove rewrites drawn from previous work. Second, the first formal proof of the PikeVM algorithm used in many real-world engines. In contrast with the specification and other formalization work, our semantics captures not only the top-priority match, but a full backtracking tree recording all possible matches and their respective priority. All our definitions and results have been mechanized in the Rocq proof assistant.

我们为现代正文表达语言提供了第一个机械化、简洁、实用、完整和经过实践证明真实的语义,并附有回溯性语义。我们通过证明它与先前存在的ECMAScript正式的JavaScript常规表达方式的逐行嵌入相当,确保了它的忠实性。我们展示了两种现实世界应用,显示了它的实用性。首先,现代正文表达方式的上下文等同性的新概念,我们用它来证明或否定以往工作中的重写。第二,许多真实世界引擎使用的PikevM算法的第一个正式证据。与规格和其他正规化工作不同的是,我们的语义学不仅捕捉了最优先的匹配,而且捕捉了记录所有可能的匹配和各自优先事项的全反跟踪树。我们的所有定义和结果在Rocq验证助理中都被机械化了。

Article 4

Title@2025-07-17 (4): Syntax Repair as Language Intersection

Title: Syntax Repair as Language Intersection Syntax-Reparatur als Sprach-Intersektion 语法修理作为语言交汇处 2507.11873v2

Authors (1): Breandan Considine

We introduce a new technique for repairing syntax errors in arbitrary context-free languages. This technique models syntax repair as a language intersection problem by defining a finite language that provably generates every syntactically valid repair within a given edit distance. Leveraging a theoretical connection between the Bar-Hillel construction from formal language theory and CFL reachability from program analysis, we show that repairability in a finite number of typographic edits is polylogarithmic parallel time decidable and provide an enumeration algorithm based on the Brzozowski derivative. Finally, we evaluate this algorithm and its implementation, demonstrating state-of-the-art results on a Python syntax repair benchmark.

我们引入了一种在任意的无背景语言中修复语法错误的新技术。 这个技术模型将语法修复作为一种语言交叉问题, 定义一种有限的语言, 可以在一定的编辑距离内生成每一种在同步上有效的修复。 我们从正式的语言理论中将Bar- Hillel 建筑的理论联系与 CFL 的可达性从程序分析中加以利用, 我们显示, 数量有限的印刷编辑的可修复性是多词性平行时间的分解, 并提供基于 Brzozowski 衍生物的查点算法。 最后, 我们评估了这一算法及其实施, 展示了 Python 语法修复基准的最新结果 。

Article 5

Title@2025-07-16 (3): Compiling a Q# Subset to QASM 3.0 in TypeScript via a JSON Based IR

Title: Compiling a Q# Subset to QASM 3.0 in TypeScript via a JSON Based IR Kompilieren eines Q#-Untersatzes zu QASM 3.0 in TypeScript über eine JSON-basierte IR 在类型Script中通过基于 JSON 的 IR 计算 QASM 3. 0 的 QASM 子集 2506.23407v2

Authors (1): Marcus Edwards

We implement a compile toolchain from Q# to QASM 3.0 including a full-featured lexer and parser implementation, as well as a compiler that supports a subset of Q# features. The lexer, parser and compiler are shown to work with various input Q# programs and the implementation is compared against existing Q# compile tools. Unlike the Microsoft implementation of the official Q# compile toolchain, our implementation is written in TypeScript in order to port functionality to web environments.

我们实施了从至QASM3.0的汇编工具链,包括全功能词汇和剖析器实施,以及一个支持子集特征的汇编器。词典、剖析器和汇编器被显示与各种输入程序一起工作,并且与现有的汇编工具进行比较。与微软实施官方的汇编工具链不同,我们的实施用TypeScript书写,以便将功能移植到网络环境。

Article 6

Title@2025-07-16 (3): An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report)

Title: An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report) Ein algebraischer Ansatz zur asymmetrischen Delegation und polymorphen Label-Inferenz (Technischer Bericht) 对非对称授权和多色标签诱导法采用代数法(技术报告) 2504.20432v2

Authors (3): Silei Ren, Coşku Acay, Andrew C. Myers

Language-based information flow control (IFC) enables reasoning about and enforcing security policies in decentralized applications. While information flow properties are relatively extensional and compositional, designing expressive systems that enforce such properties remains challenging. In particular, it can be difficult to use IFC labels to model certain security assumptions, such as semi-honest agents. Motivated by these modeling limitations, we study the algebraic semantics of lattice-based IFC label models, and propose a semantic framework that allows formalizing asymmetric delegation, which is partial delegation of confidentiality or integrity. Our framework supports downgrading of information and ensures their safety through nonmalleable information flow (NMIF). To demonstrate the practicality of our framework, we design and implement a novel algorithm that statically checks NMIF and a label inference procedure that efficiently supports bounded label polymorphism, allowing users to write code generic with respect to labels.

以语言为基础的信息流通控制(IFC)有助于在分散应用中推理和执行安全政策。信息流通特性相对来说是扩展性的,构成性的,但设计执行这种特性的表达系统仍然具有挑战性。特别是,可能难以使用IFC标签来模拟某些安全假设,例如半诚实剂。受这些模型限制的驱使,我们研究了基于 lattice 的IFC标签模型的代数语义,并提出了一个语义框架,使不对称代表团正规化,这是部分保密性或完整性的下放。我们的框架支持信息降级,并通过不可移动的信息流动(NMIF)确保其安全。为了展示我们框架的实用性,我们设计和实施一种新的算法,静态地检查NMIF和一个有效支持受约束的标签多形态的标签推断程序,允许用户在标签方面编写通用代码。

Article 7

Title@2025-07-16 (3): Dual-Numbers Reverse AD for Functional Array Languages

Title: Dual-Numbers Reverse AD for Functional Array Languages Dual-Nummern Reverse AD für funktionale Array-Sprachen 功能阵列语言双倍反向反向 2507.12640v1

Authors (4): Tom Smeding, Mikołaj Konarski, Simon Peyton Jones, Andrew Fitzgibbon

The standard dual-numbers construction works well for forward-mode automatic differentiation (AD) and is attractive due to its simplicity; recently, it also has been adapted to reverse-mode AD, but practical performance, especially on array programs, leaves a lot to be desired. In this paper we introduce first-class support for multidimensional arrays in dual-numbers reverse-mode AD with little to no performance overhead. The algorithm consists of three loosely-coupled components: a semantics-preserving vectorisation code transformation (the bulk-operation transform or BOT), a fairly straightforward lifting of the basic dual-numbers reverse AD algorithm to a mostly first-order array language, and symbolic interpretation to achieve an end-to-end compilation pipeline. Unfortunately, we lose some of the nice generalisable aspects of dual-numbers AD in the process, most importantly support for higher-order code. We do support some higher-order array combinators, but only a carefully-chosen set: ‘build’ (elementwise array construction), ‘gather’ and ‘scatter’. In return, the BOT can eliminate the essential (for AD) higher-orderness of the input program, meaning that AD gets essentially presented with a first-order program. This allows the naive trick of lifting dual numbers to “dual arrays” to work without much modification.

标准的双数字构造对于前方模式自动区分( AD) 效果良好,并且由于其简单性而具有吸引力; 最近,它也适应了反向模式自动区分( AD) , 但实际性能, 特别是在阵列程序上, 仍有许多有待改进之处。 在本文中, 我们引入了以双数反向模式对多维阵列的一流支持, 反向模式自动区分( AD) , 几乎没有或没有性能管理。 算法由三个松散的组合组成: 语义- 保留矢量代码转换( 批量操作变换 或 BOT) , 将基本双数反向自动算法直截直升为多数一阶阵列语言, 以及象征性的翻译, 以达到端到端到端的编织编织管道。 不幸的是, 我们失去了双数 ADAD( 最重要的是支持高调码) 的一些简单化阵列组合组合组合组合, 但只有精心挑选的组合 : “ 重建 ” ( 快速阵列建设 ) , “ ” 和“ ” 和“ 平坦” , 这样, BODAD- transport (基本地) 可以取消了双轨的双向高级程序。

Article 8

Title@2025-07-16 (3): Modeling Open-World Cognition as On-Demand Synthesis of Probabilistic Models

Title: Modeling Open-World Cognition as On-Demand Synthesis of Probabilistic Models Modellierung der Open-World-Kognition als On-Demand-Synthese probabilistischer Modelle 将开放世界的认知建模作为概率模型的 “ 现场合成 “ 模型 2507.12547v1

Authors (11): Lionel Wong, Katherine M. Collins, Lance Ying, Cedegao E. Zhang, Adrian Weller, Tobias Gersternberg, Timothy O’Donnell, Alexander K. Lew, Jacob D. Andreas, Joshua B. Tenenbaum, Tyler Brooke-Wilson

When faced with novel situations, people are able to marshal relevant considerations from a wide range of background knowledge and put these to use in inferences and predictions. What permits us to draw in globally relevant information and reason over it coherently? Here, we explore the hypothesis that people use a combination of distributed and symbolic representations to construct bespoke mental models tailored to novel situations. We propose a computational implementation of this idea – a ``Model Synthesis Architecture’’ (MSA) – using language models to implement global relevance-based retrieval and model synthesis and probabilistic programs to implement bespoke, coherent world models. We evaluate our MSA as a model of human judgments on a novel reasoning dataset. The dataset – built around a Model Olympics domain of sports vignettes – tests models’ capacity for human-like, open-ended reasoning by requiring (i) judgments about novel causal structures described in language; (ii) drawing on large bodies of background knowledge; and (iii) doing both in light of observations that introduce arbitrary novel variables. Our MSA approach captures human judgments better than language model-only baselines, under both direct and chain-of-thought generations from the LM that supports model synthesis. These results suggest that MSAs can be implemented in a way that mirrors people’s ability to deliver locally coherent reasoning over globally relevant variables, offering a path to understanding and replicating human reasoning in open-ended domains.

在面临新情况时,人们能够从广泛的背景知识中汇集相关考虑,并将这些因素用于推论和预测。什么能使我们在全球范围内以一致的方式获取相关信息和理性?在这里,我们探讨一种假设,即人们使用分布式和象征式的表达方式相结合来构建符合新情况的精神模型;我们建议对这一概念进行计算实施 – – “ 模型综合综合架构 “ (MSA) – – 使用语言模型来实施基于全球相关性的检索和模型合成,以及概率化方案,以实施直观、一致的世界模型。我们评估我们的特派任务生活津贴,将其作为人类对新推理数据集的判断模型。数据集 – – 围绕“奥林匹克运动”运动“体育名流域 – – 测试模型” 来为人性、开放型的推理能力而构建。我们建议(一) 判断语言中描述的新因果结构;(二) 借鉴大量的背景知识;以及(三) 结合引入任意的新变数的观察,既能反映人类的人类的判断,又能更好理解语言模型的基线,在直接和连锁推理学能力下,能够从全球推理推算出人类的推理结果。

Article 9

Title@2025-07-16 (3): LLM-Based Config Synthesis requires Disambiguation

Title: LLM-Based Config Synthesis requires Disambiguation LLM-basierte Konfig-Synthese erfordert Disambiguation 基于 LLM 的配置合成要求差异化 2507.12443v1

Authors (5): Rajdeep Mondal, Nikolaj Bjorner, Todd Millstein, Alan Tang, George Varghese

Beyond hallucinations, another problem in program synthesis using LLMs is ambiguity in user intent. We illustrate the ambiguity problem in a networking context for LLM-based incremental configuration synthesis of route-maps and ACLs. These structures frequently overlap in header space, making the relative priority of actions impossible for the LLM to infer without user interaction. Measurements in a large cloud identify complex ACLs with 100’s of overlaps, showing ambiguity is a real problem. We propose a prototype system, Clarify, which uses an LLM augmented with a new module called a Disambiguator that helps elicit user intent. On a small synthetic workload, Clarify incrementally synthesizes routing policies after disambiguation and then verifies them. Our treatment of ambiguities is useful more generally when the intent of updates can be correctly synthesized by LLMs, but their integration is ambiguous and can lead to different global behaviors.

除了幻觉之外,使用LLMs的程序合成还存在另一个问题,即用户用意模糊不清。我们举例说明了基于LLM的路线图和ACLS的递增配置合成的网络环境中的模糊问题。这些结构在页眉空间中经常重叠,使得LLM无法在没有用户互动的情况下推断行动的相对优先性。在大云中测量出复杂的ACLs和100的重叠情况,显示出模糊不清是一个真正的问题。我们建议了一个原型系统,Clarify,它使用一种LLM, 并配有一个新的模块, 称为“辨别器”, 帮助激发用户的意向。在小型合成工作量中, 澄清递增合成了路线政策, 并在进行校验。 当LMs能够正确合成更新的意图时, 我们对于模糊之处的处理更为普遍有用, 但是它们的整合是模糊不清的, 并可能导致不同的全球行为。

Article 10

Title@2025-07-16 (3): GitChameleon: Evaluating AI Code Generation Against Python Library Version Incompatibilities

Title: GitChameleon: Evaluating AI Code Generation Against Python Library Version Incompatibilities GitChameleon: Bewertung der KI-Code-Generation gegen Python Library Version Inkompatibilitäten GitChameleon:评估AI 与 Python 图书馆版本不兼容性 2507.12367v1

Authors (12): Diganta Misra, Nizar Islah, Victor May, Brice Rauby, Zihan Wang, Justine Gehring, Antonio Orvieto, Muawiz Chaudhary, Eilif B. Muller, Irina Rish, Samira Ebrahimi Kahou, Massimo Caccia

The rapid evolution of software libraries poses a considerable hurdle for code generation, necessitating continuous adaptation to frequent version updates while preserving backward compatibility. While existing code evolution benchmarks provide valuable insights, they typically lack execution-based evaluation for generating code compliant with specific library versions. To address this, we introduce GitChameleon, a novel, meticulously curated dataset comprising 328 Python code completion problems, each conditioned on specific library versions and accompanied by executable unit tests. GitChameleon rigorously evaluates the capacity of contemporary large language models (LLMs), LLM-powered agents, code assistants, and RAG systems to perform version-conditioned code generation that demonstrates functional accuracy through execution. Our extensive evaluations indicate that state-of-the-art systems encounter significant challenges with this task; enterprise models achieving baseline success rates in the 48-51\% range, underscoring the intricacy of the problem. By offering an execution-based benchmark emphasizing the dynamic nature of code libraries, GitChameleon enables a clearer understanding of this challenge and helps guide the development of more adaptable and dependable AI code generation methods. We make the dataset and evaluation code publicly available at https://github.com/mrcabbage972/GitChameleonBenchmark.

软件图书馆的迅速演变为代码生成带来了相当大的障碍,需要不断适应经常更新版本,同时保持后向兼容性。虽然现有的代码演变基准提供了宝贵的洞察力,但它们通常缺乏基于执行的评价,以生成符合特定图书馆版本的代码。为了解决这个问题,我们引入了GitChameleon,这是一套由328个Python代码完成问题组成的新颖、精心整理的数据集,每套数据都以特定图书馆版本为条件,并伴之以可执行单位测试。GitChameleon严格评估当代大型语言模型(LLLMS)、LLM-动力代理、代码助理和RAG系统的能力,以实施显示功能准确性,进行版本定制的代码生成。我们的广泛评估表明,最先进的系统在这项工作中遇到重大挑战;企业模型在48-51范围内实现了基线成功率,凸显了问题的严重性。通过提供基于执行的基准,强调代码图书馆的动态性质,GitChameleon能够更清楚地了解这一挑战,并帮助指导开发更适应性和更可靠的AI代码生成方法。我们在http://Gsmasmasm上公开提供数据设置和评估系统。

Article 11

Title@2025-07-16 (3): Programming Distributed Collective Processes in the eXchange Calculus

Title: Programming Distributed Collective Processes in the eXchange Calculus Programmierung verteilter kollektiver Prozesse im eXchange Calculus eXchange Calculus 中的程序编程分配集体进程 2401.11212v5

Authors (5): Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Gianluca Torta, Mirko Viroli

Recent trends like the Internet of Things (IoT) suggest a vision of dense and multi-scale deployments of computing devices in nearly all kinds of environments. A prominent engineering challenge revolves around programming the collective adaptive behaviour of such computational ecosystems. This requires abstractions able to capture concepts like ensembles (dynamic groups of cooperating devices) and collective tasks (joint activities carried out by ensembles). In this work, we consider collections of devices interacting with neighbours and that execute in nearly-synchronised sense-compute-interact rounds, where the computation is given by a single program mapping sensing values and incoming messages to output and outcoming messages. To support programming whole computational collectives, we propose the abstraction of a distributed collective process, which can be used to define at once the ensemble formation logic and its collective task. We formalise the abstraction in the eXchange Calculus (XC), a core functional language based on neighbouring values (maps from neighbours to values) where state and interaction is handled through a single primitive, exchange, and provide a corresponding implementation in the FCPP language. Then, we exercise distributed collective processes using two case studies: multi-hop message propagation and distributed monitoring of spatial properties. Finally, we discuss the features of the abstraction and its suitability for different kinds of distributed computing applications.

在这项工作中,我们考虑与邻居发生互动的装置的集成,这些装置以近同步的感知和计算互动周期执行,计算方法是由一个单一程序绘制感测值和发送信息到输出和流出信息。为了支持整个计算集体的编程,我们提议一个分布式集体过程的抽象化,这个过程可以用来立即界定共性形成逻辑及其集体任务。我们把电子Xchange Calculus(XC)中的抽象化,这是一个基于相邻价值的核心功能语言(从邻居到价值观的图解),通过单一原始、交换处理国家和互动,并在FCPP语言中提供相应的执行。最后,我们利用两种案例研究,进行分布式集成的集体进程,并传播各种空间信息。最后,我们用两种案例研究的形式,进行集体分布式的数学特性。我们用两种案例研究来传播其空间信息。最后,我们用两种案例研究来传播空间信息。

Article 12

Title@2025-07-16 (3): Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

Title: Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs Nanopass-Rückübersetzung von Call-Return-Bäumen für mechanisierte sichere Compilations-Proofs 机械化安全编译证明调回回树的纳米通回转换 2503.19609v3

Authors (3): Jérémy Thibault, Joseph Lenormand, Catalin Hritcu

Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversarial target context can mount against the compiled program. Proving that these compilation chains are secure is, however, challenging, and involves a non-trivial back-translation step: for any attack a target context mounts against the compiled program one has to exhibit a source context mounting the same attack against the source program. We describe a novel back-translation technique, which results in simpler proofs that can be more easily mechanized in a proof assistant. Given a finite set of finite trace prefixes, capturing the interaction recorded during an attack between a target context and the compiled program, we build a call-return tree that we back-translate into a source context producing the same trace prefixes. We use state in the generated source context to record the current location in the call-return tree. The back-translation is done in several small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove this back-translation correct we give semantics to every intermediate call-return tree language, using ghost state to store information and explicitly enforce execution invariants. We prove several small forward simulations, basically seeing the back-translation as a verified nanopass compiler. Thanks to this modular structure, we are able to mechanize this complex back-translation and its correctness proof in the Rocq prover without too much effort.

研究者的目标是建立安全的编译链, 表明如果源环境没有攻击, 源环境可以对源程序发动攻击, 那么也没有攻击。 证明这些编译链是安全的, 然而, 具有挑战性, 并涉及非三轨反译步骤 : 任何针对编译程序的攻击, 一个目标环境会显示一个源环境, 对源程序发动同样的攻击。 我们描述一种新型反译技术, 其结果是更简单的证明, 可以在一个校对助理中进行机械化。 鉴于有一套有限的追踪前缀, 捕捉在目标环境与编译程序之间攻击时记录的互动, 我们建立一个呼呼回树, 我们再转换成一个源环境, 产生一个相同的追踪前缀。 我们在生成的源环境里使用状态来记录当前在调回树中进行同样的攻击。 后翻是几个小步骤, 每进一次新的信息, 说明该地点应该如何变化, 取决于环境重新控制。 为了证明这个调时, 我们用这个调回流树结构, 基本地证明, 我们用一个中间的变压, 将一个精度 。

Article 13

Title@2025-07-16 (3): Dependent Multiplicities in Dependent Linear Type Theory

Title: Dependent Multiplicities in Dependent Linear Type Theory Abhängige Vielfältigkeit in der abhängigen Lineartyptheorie 依附线类类型理论中的依附倍数 2507.08759v2

Authors (1): Maximilian Doré

We present a novel dependent linear type theory in which the multiplicity of some variable - i.e., the number of times the variable can be used in a program - can depend on other variables. This allows us to give precise resource annotations to many higher-order functions that cannot be adequately typed in any other system. Inspired by the Dialectica translation, our typing discipline is obtained by embedding linear logic into dependent type theory and specifying how the embedded logic interacts with the host theory. We can then use a standard natural numbers type to obtain a quantitative typing system with dependent multiplicities. We characterise the semantics for our theory as a combination of standard models of dependent type theory and linear logic. Our system can be added to any dependently typed language, which we demonstrate with an implementation in Agda.

我们提出了一个新颖的依附线性理论,在这个理论中,某些变量的多重性,即该变量在程序中使用的次数,可以取决于其他变量。这使我们能够为许多无法在任何其他系统中适当打字的更高层次的函数提供精确的资源说明。在对数翻译的启发下,我们的打字纪律是通过将线性逻辑嵌入从数性理论,并具体说明嵌入的逻辑如何与主机理论相互作用而获得的。然后,我们可以使用标准的自然数字类型来获得一个具有依附多重性的定量打字系统。我们把理论的语义定性为依赖类型理论和线性逻辑的标准模型的组合。我们的系统可以添加到任何依附的打字语言中,我们在阿格达语中演示了这些语言。

Article 14

Title@2025-07-16 (3): Optimized Execution of FreeCHR

Title: Optimized Execution of FreeCHR Optimierte Ausführung von FreeCHR 最优化地执行自由人权委员会 2506.14485v2

Authors (2): Sascha Rechenberger, Thom Frühwirth

Constraint Handling Rules (CHR) is a rule-based programming language that rewrites collections of constraints. It is typically embedded into a general-purpose language. There exists a plethora of implementation for numerous host languages. However, the existing implementations often re-invent the method of embedding, which impedes maintenance and weakens assertions of correctness. To formalize and thereby standardize the embedding of a ground subset of CHR into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical CHR. For the sake of simplicity, abstract implementations of our framework did not yet include a concrete matching algorithm nor optimizations. In this paper, we introduce an improved execution and matching algorithm for FreeCHR. We also provide empirical evaluation of the algorithm.

约束性处理规则(CHR)是一种基于规则的编程语言,它重写了各种制约的汇编,通常被嵌入一种通用语言中。对于许多主机语言,存在着大量的实施。然而,现有的实施常常重新发明了嵌入方法,这妨碍了维护,削弱了正确性的说法。为使将CHR的一小块地嵌入到任意主机语言中的做法正规化并从而实现标准化,我们引入了FreeICHR框架,并证明它是传统的CHHR的有效代表。为了简单起见,我们框架的抽象实施还没有包含具体的匹配算法或优化。在本文中,我们为FreeICHR引入了一个更好的执行和匹配算法。我们还对算法进行了经验性评估。

Article 15

Title@2025-07-16 (3): Towards Relational Contextual Equality Saturation

Title: Towards Relational Contextual Equality Saturation Auf dem Weg zu einer relationalen kontextuellen Gleichstellungssättigung 走向关系背景平等饱和 2507.11897v1

Authors (3): Tyler Hou, Shadaj Laddad, Joseph M. Hellerstein

Equality saturation is a powerful technique for program optimization. Contextual equality saturation extends this to support rewrite rules that are conditioned on where a term appears in an expression. Existing work has brought contextual reasoning to egg; in this paper, we share our ongoing work to extend this to relational equality saturation in egglog. We summarize the existing approaches to contextual equality saturation, outline its main applications, and identify key challenges in combining this approach with relational models.

平等饱和是优化方案的有力技术。 上下文平等饱和将之扩展至支持以某一术语出现时为条件的重写规则。 现有工作带来了相关推理;在本文件中,我们分享了我们正在进行的工作,以将之扩大到蛋蛋中的平等饱和。 我们总结了当前实现背景平等饱和的方法,概述了其主要应用,并找出了将这一方法与关系模型相结合的主要挑战。

Article 16

Title@2025-07-16 (3): Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers

Title: Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers Universelle Synthese von differenzierbaren numerischen Abstrakttransformatoren 不同金枪鱼可有区别的量化数字抽象变异器通用合成 2507.11827v1

Authors (3): Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh

Numerical abstract interpretation is a widely used framework for the static analysis of numerical programs. However, existing numerical abstract interpreters rely on hand-crafted, instruction-specific transformers tailored to each domain, with no general algorithm for handling common operations across domains. This limits extensibility, prevents precise compositional reasoning over instruction sequences, and forces all downstream tasks to use the same fixed transformer regardless of their precision, efficiency, or task-specific requirements. To address these limitations, we propose a universal transformer synthesis algorithm that constructs a parametric family of sound abstract transformers for any given polyhedral numerical domain and a concrete operator from the class of Quadratic-Bounded Guarded Operators (QGO), which includes both individual instructions and structured sequences. Each instantiation in this family is sound by construction, enabling downstream analyses to adapt the transformer to their particular needs. The space of transformers is differentiable but complex. To efficiently explore this space of transformers, we introduce the Adaptive Gradient Guidance (AGG) procedure, a gradient-guided search strategy that steers the search process based on downstream analysis objectives and runtime constraints. We implement these ideas in the USTAD framework and evaluate their effectiveness across three numerical abstract domains: Zones, Octagons, and Polyhedra. Our results demonstrate that the universal synthesis algorithm successfully constructs sound families of transformers across domains, and that USTAD achieves significant, tunable precision gains over baselines by leveraging compositional reasoning and efficient gradient-guided traversal of the transformer space.

数字抽象解释是一个广泛用于对数字程序进行静态分析的框架。然而,现有的数字抽象翻译依赖根据每个领域量身定制的手制、针对具体指示的变压器,没有处理跨域共同操作的一般算法。这限制了可扩展性,妨碍了对指令序列的精确构成推理,迫使所有下游任务使用相同的固定变压器,而不论其精确性、效率或具体任务要求如何。为了解决这些限制,我们建议了一个通用变压器合成算法,为任何给定的多面性数字域构建一个由健全的抽象变压器组成的准组,以及一个来自夸德-弯式保护操作器(QGO)类别的具体操作器,该变压器既包括单个指示和结构序列。这一组的每个即时性推法都是由建筑设计的,使下游分析器能够适应其特定需要。变压器的空间不同,但复杂。为了有效地探索变压器的这一空间,我们引入了适应性变压器(AGG)程序,一个由梯式调整的搜索战略来指导搜索过程,它根据下游流-弯式变压式变压变压变压变压的变压的变压的变压变压器的变压器的变压法,根据下精法的变压的变压的变压的变压的变压器的变压法,我们数的变压的变压的变压的变压法框架,用法,我们数的变压的变压的变压的变压的变压的变压的变压的变压法,我们的变压的变压的变压的变压的变压的变压的变压法框架,用法,用法,用法,用法,我们用法,我们用的变压的变压的变压的变压的变压的变压的变压的变法,我们用法,用法,用法,在了整个的变压的变压的变压的变压的变压的变压的变压的变压的变压的变压的变压的变法,我们的变法,我们的变法,我们的变压的变的变法, 的变压的变压的变法,我们的变压的变法,我们的变压的变法

Article 17

Title@2025-07-15 (2): A Practical Quantum Hoare Logic with Classical Variables, I

Title: A Practical Quantum Hoare Logic with Classical Variables, I Eine praktische Quantenhoare-Logik mit klassischen Variablen, I 具有古典变量的实用量子 Hoare 逻辑,I 2412.09869v2

Authors (1): Mingsheng Ying

In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterised by classical variables). These specifications offer greater clarity and align more closely with the programmer’s intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification.

在本文中,我们用古典变数计算量子方案的推理提供了一种Hoare式逻辑逻辑。我们的方法比以往的工作有几项改进:(1) 增强编程语言的表达性:(1) 我们的逻辑适用于包含量子阵列和参数化量子门的古典变数逻辑的量子方案,以前关于量子阵列和参数化量子门的研究没有涉及这些变量。 (2) 直观的正确性规格: 在我们的逻辑、先决条件和条件中,用古典变数计算量子的量子方案,被指定为由古典一阶逻辑公式和量级上游公式(可能由古典变数加以比较的参数)组成的对子方案。这些规格提供了更大的清晰度,与程序对量子和古典相互作用的直观理解更加一致。 (3) 简化的验证系统:在为量子量子计量的推理法制定证据规则时引入了一种新概念,同时(2) 我们为量子程序开发了一个证明系统,只需要对古典Hoare逻辑作最低限度的修改。此外,这种证明系统可以有效而方便地与古典的一级一级一阶逻辑结合,以核查古典变的量子程序。作为结果,用于对古典化的校正化的核查技术进行较容易的校准程序。

Article 18

Title@2025-07-15 (2): Picat Through the Lens of Advent of Code

Title: Picat Through the Lens of Advent of Code Picat durch die Adventslinse des Kodex 透过法典修道院的透镜 2507.11731v1

Authors (4): Neng-Fa Zhou, Cristian Grozea, Håkan Kjellerstrand, Oisín Mac Fhearaí

Picat is a logic-based, multi-paradigm programming language that integrates features from logic, functional, constraint, and imperative programming paradigms. This paper presents solutions to several problems from the 2024 Advent of Code (AoC). While AoC problems are not designed for any specific programming language, certain problem types, such as reverse engineering and path-finding, are particularly well-suited to Picat due to its built-in constraint solving, pattern matching, backtracking, and dynamic programming with tabling. This paper demonstrates that Picat’s features, especially its SAT-based constraint solving and tabling, enable concise, declarative, and highly efficient implementations of problems that would require significantly more effort in imperative languages.

Picat是一种基于逻辑的多式编程语言,结合了逻辑、功能、制约和必要编程范式的特征,本文件介绍了2024年《守则》基督复临会(AoC)的若干问题的解决办法。虽然AoC问题不是针对任何具体的编程语言设计的,但某些类型的问题,如逆向工程和路由调查,特别适合Picat,因为Picat的内在局限性解决、模式匹配、反向跟踪和动态编程与制表。本文表明,Picat的特征,特别是基于SAT的制约因素的解决和制表,能够简洁、宣示和高效地解决需要用迫切语言做出更大努力的问题。

Article 19

Title@2025-07-15 (2): Quantum circuits are just a phase

Title: Quantum circuits are just a phase Quantenschaltungen sind nur eine Phase 量子电路只是一个阶段 2507.11676v1

Authors (4): Chris Heunen, Louis Lemonnier, Christopher McNally, Alex Rice

Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a novel yet simple quantum programming language for generating unitaries from “just a phase”; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the “if let” construct that captures subspace selection via pattern matching. This minimal language lifts the focus from quantum gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover’s search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

今天的量子程序是在低程度的抽象-量子电路与组装语言类似-甚至先进的量子编程语言基本上作为电路描述语言而发挥作用。这种状态妨碍了可缩放性、清晰度和对更高层次推理的支持。 需要更多的抽象和直观的量子编程结构。 为此,我们引入了一种新颖而简单的量子编程语言,用于从“ 仅仅一个阶段” 生成单词; 我们结合了一个(全球)阶段操作,以“ 如果允许” 结构的量子类比来捕捉到子空间选择的量子。 这种最小语言将重点从量子门提升到电流结构变异、 调和受控的单位; 在量算法设计中,我们以几种方式展示我们语言的表达力。 首先,我们确定我们的代表性是普遍性的,通过一个通用的量子门设置。 第二,我们展示重要的量子算法可以自然和简洁的表达, 包括 Grover的搜索算法、汉密尔顿式模拟、 量子转换、 量子变换、 量级变换、 调和受控控的单位化; 共同的构算的构算。我们最后的精化的精化、 将这些结构化、 的顺序化、 使这些结构化的顺序的量值的量值化、 使我们最终的量子化,让我们化、 将这些直路流的顺序化,我们的顺序化,我们的顺序化、 的顺序化、 的顺序化、 的顺序化,我们的顺序化、 的顺序化,我们的顺序化、 的顺序化,我们的顺序化、 的顺序化、直序式的顺序化。

Article 20

Title@2025-07-15 (2): On the Complexity of Checking Mixed Isolation Levels for SQL Transactions

Title: On the Complexity of Checking Mixed Isolation Levels for SQL Transactions Über die Komplexität der Überprüfung gemischter Isolationsebenen für SQL-Transaktionen 关于SQL交易核对混合混合隔离水平的复杂性 2505.18409v3

Authors (3): Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo

Concurrent accesses to databases are typically grouped in transactions which define units of work that should be isolated from other concurrent computations and resilient to failures. Modern databases provide different levels of isolation for transactions that correspond to different trade-offs between consistency and throughput. Quite often, an application can use transactions with different isolation levels at the same time. In this work, we investigate the problem of testing isolation level implementations in databases, i.e., checking whether a given execution composed of multiple transactions adheres to the prescribed isolation level semantics. We particularly focus on transactions formed of SQL queries and the use of multiple isolation levels at the same time. We show that many restrictions of this problem are NP-complete and provide an algorithm which is exponential-time in the worst-case, polynomial-time in relevant cases, and practically efficient.

数据库的平行存取通常按交易分类,这些交易确定的工作单位应与同时进行的其他计算分开,并具有抵御失败的能力;现代数据库对符合一致性和吞吐量之间不同权衡交易的不同交易提供不同程度的隔离。非常常见的情况是,应用程序可以同时使用不同隔离水平的交易;在这项工作中,我们调查在数据库中测试隔离水平执行的问题,即检查由多个交易组成的特定执行是否遵守了规定的隔离等级语义。我们特别侧重于由SQL查询组成的交易以及同时使用多重隔离等级。我们表明,这一问题的许多限制是NP的,提供了一种在最坏情况下是指数性的、在相关情况下是多元时间的、而且实际有效的算法。

Article 21

Title@2025-07-15 (2): The downgrading semantics of memory safety

Title: The downgrading semantics of memory safety Die abwertende Semantik der Speichersicherheit 内存安全词义的降级 2507.11282v1

Authors (3): René Rydhof Hansen, Andreas Stenbæk Larsen, Aslan Askarov

Memory safety is traditionally characterized in terms of bad things that cannot happen, an approach that is often criticized as unprincipled. Prior work suggest a connection between memory safety and noninterference, but no satisfactory semantic notion of memory safety is currently known. This work proposes a notion of gradual allocator independence that accurately captures many allocator-specific aspects of memory safety. We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways to account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

记忆安全的传统特征是无法发生的坏事,这种方法常常被批评为没有原则。 先前的工作表明记忆安全与不干涉之间的联系,但目前尚没有令人满意的记忆安全语义概念。 这项工作提出了一个逐渐分配独立的概念, 精确地捕捉了记忆安全中许多偏移特性的具体方面。 我们考虑一种低层次的语言,可以使用一个在平坦的记忆模型中提供中枢和自由原始的缩放器。 指针只是整数, 因而写出记忆- 不安全的程序是微不足道的。 逐渐分配独立的基本直觉是不干涉, 即分配器不得影响程序执行。 这种直觉在两种重要方面得到细化, 以说明正在运行超模量的分配器和编程程序有点向内导的投射器。 定义的关键洞察是将这些扩展作为降级的形式对待, 并给予它们令人满意的技术待遇, 使用最先进的信息流动机制 。

Article 22

Title@2025-07-14 (1): Stream programs are monoid homomorphisms with state

Title: Stream programs are monoid homomorphisms with state Stream-Programme sind monoide Homomorphismen mit Zustand 溪流方案是单一单一的同质状态方案 2507.10799v1

Authors (3): Tyler Hou, Michael Arntzenius, Max Willsey

We define a broad class of deterministic stream functions and show they can be implemented as homomorphisms into a “state” monoid. The homomorphism laws are simpler than the conditions of previous semantic frameworks for stream program optimization, yet retain support for rich equational reasoning over expressive dataflow programs, including sequential composition, parallel composition, and feedback. We demonstrate this using examples of partitioned database joins, stratified negation, and a simplified model of TCP.

我们定义了广泛的确定性流函数类别,并表明这些函数可以作为“状态”单体执行。 单体法比以往流程序优化的语义框架更为简单,但依然支持关于表达性数据流程序的丰富的等式推理,包括相继构成、平行组成和反馈。 我们用分隔式数据库连接、分层否定和简化TCP模式的例子来证明这一点。

Article 23

Title@2025-07-14 (1): Speculative Automated Refactoring of Imperative Deep Learning Programs to Graph Execution

Title: Speculative Automated Refactoring of Imperative Deep Learning Programs to Graph Execution Spekulative Automatisierte Refaktorisierung imperativer Deep Learning-Programme zur Graphen-Execution 用于图表执行的势必深深学习方案的投机性自动重组 2504.05424v3

Authors (5): Raffi Khatchadourian, Tatiana Castro Vélez, Mehdi Bagherzadeh, Nan Jia, Anita Raja

Efficiency is essential to support ever-growing datasets, especially for Deep Learning (DL) systems. DL frameworks have traditionally embraced deferred execution-style DL code – supporting symbolic, graph-based Deep Neural Network (DNN) computation. While scalable, such development is error-prone, non-intuitive, and difficult to debug. Consequently, more natural, imperative DL frameworks encouraging eager execution have emerged but at the expense of run-time performance. Though hybrid approaches aim for the “best of both worlds,” using them effectively requires subtle considerations. Our key insight is that, while DL programs typically execute sequentially, hybridizing imperative DL code resembles parallelizing sequential code in traditional systems. Inspired by this, we present an automated refactoring approach that assists developers in determining which otherwise eagerly-executed imperative DL functions could be effectively and efficiently executed as graphs. The approach features novel static imperative tensor and side-effect analyses for Python. Due to its inherent dynamism, analyzing Python may be unsound; however, the conservative approach leverages a speculative (keyword-based) analysis for resolving difficult cases that informs developers of any assumptions made. The approach is: (i) implemented as a plug-in to the PyDev Eclipse IDE that integrates the WALA Ariadne analysis framework and (ii) evaluated on nineteen DL projects consisting of 132 KLOC. The results show that 326 of 766 candidate functions (42.56%) were refactorable, and an average relative speedup of 2.16 on performance tests was observed with negligible differences in model accuracy. The results indicate that the approach is useful in optimizing imperative DL code to its full potential.

效率对于支持不断增长的数据集至关重要, 特别是深海学习( DL) 系统。 DL 框架传统上采用推迟执行式 DL 代码, 支持符号性、 基于图形的深神经网络( DNN) 计算。 虽然可以缩放, 但这种开发是容易出错的, 非直观的, 并且难以调试。 因此, 更自然的、 必要的 DL 框架鼓励急迫执行, 但却牺牲了运行时的性能。 虽然混合方法旨在“ 最佳世界” , 有效地使用它们需要微妙的考虑。 我们的关键洞察力是, DL 程序通常按顺序执行, 混合的 DL 代码类似于传统系统中的平行代码。 受此启发, 我们提出了一个自动重构的重构方法, 帮助开发者确定哪些否则急迫地执行的 DL 功能可以有效和高效地作为图表执行。 这种方法以新颖的静态 高压和副效果分析为Python 。 由于它固有的活力, 分析Python 可能是不准确的; 但是, 保守方法将一个可调的 Ral- dal- dal- dal- disal- disal 函数法的精准的精准的精准的精准的精度函数在传统方法在传统的精准的精准的精准的精准的精准的精准的精准的精准的精度函数( , 。

Article 24

Title@2025-07-14 (1): Orthologic Type Systems

Title: Orthologic Type Systems Orthologische Typsysteme 矫形类型系统 2507.10482v1

Authors (2): Simon Guilloud, Viktor Kunčak

We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to extend orthologic to support monotonic and antimonotonic functions, supporting the use of type constructors in such type systems. We present a proof system for orthologic with function symbols, showing that it admits partial cut elimination. Using these insights, we present an $\mathcal O(n^2(1+m))$ algorithm for deciding the subtyping relation under $m$ assumptions. We also show $O(n^2)$ polynomial-time normalization algorithm, allowing simplification of types to their minimal canonical form.

我们建议使用正交系统作为设计支持交叉、联合和否定类型类型的类型系统的基础,并同时使用分型假设。我们展示了如何扩展正交系统以支持单声波和抗调功能,支持在此类系统中使用型建构器。我们展示了带有功能符号的正交系统证明系统,表明它承认部分消除。利用这些洞察力,我们展示了美元(m2(1+m)美元)的算法,用于在美元假设下决定亚交关系。我们还展示了美元(n%2)美元的多边时间正常化算法,允许将类型简化为最低限度的卡通形式。

Article 25

Title@2025-07-14 (1): Toolsuite for Implementing Multiagent Systems Based on Communication Protocols

Title: Toolsuite for Implementing Multiagent Systems Based on Communication Protocols Toolsuite zur Implementierung von Multiagentensystemen auf Basis von Kommunikationsprotokollen 基于通信议定书的用于实施多剂系统的工具 2507.10324v1

Authors (3): Amit K. Chopra, Samuel H. Christie V, Munindar P. Singh

Interaction-Oriented Programming (IOP) is an approach to building a multiagent system by modeling the interactions between its roles via a flexible interaction protocol and implementing agents to realize the interactions of the roles they play in the protocol. In recent years, we have developed an extensive suite of software that enables multiagent system developers to apply IOP. These include tools for efficiently verifying protocols for properties such as liveness and safety and middleware that simplifies the implementation of agents. This paper presents some of that software suite.

以互动为主的编程(IPP)是建立多试剂系统的一种方法,其方法是通过灵活的互动协议,模拟其作用与实施者之间的互动,以实现其在协议中所起作用的相互作用。近年来,我们开发了一套广泛的软件,使多试剂系统开发者能够应用IPP。其中包括有效核查诸如活性和安全等特性协议的工具,以及简化代理实施过程的中间软件。本文件介绍了其中的一些软件套件。

Article 26

Title@2025-07-14 (1): Rows and Capabilities as Modal Effects

Title: Rows and Capabilities as Modal Effects Zeilen und Fähigkeiten als Modale Effekte 作为模式效果的行和能力 2507.10301v1

Authors (2): Wenhao Tang, Sam Lindley

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide valuable insights on language design.

效果处理器允许程序员以模块形式模型和计算效果 。 效果系统静态地保证所有效果都得到处理 。 最近几个实际效果系统以行多形态或能力为基础 。 但是,在理解具有这种不同基础的效果系统之间的精确关系方面仍然存在差距 。 主要的难题是,在基于行的和基于能力的系统,效果跟踪通常与功能等其他特征交织在一起。 我们为编码、分析和比较效果系统提出了一个统一的框架 。 我们的框架利用和概括性效果类型, 这是一种最新的新颖效果系统, 通过模式对功能的跟踪产生不同影响 。 模式提供了对何时和如何跟踪效果的细化控制, 使我们能够表达不同的效果跟踪战略 。 我们把基于行的和基于能力的效果系统的编码作为宏观翻译纳入我们的框架, 并表明这些编码保存了类型和语义。 我们的编码揭示了不同效果系统的效果跟踪机制的精髓, 能够直接分析它们的差异, 并提供对语言设计的宝贵洞察力 。

Article 27

Title@2025-07-14 (1): Formal Verification of Variational Quantum Circuits

Title: Formal Verification of Variational Quantum Circuits Formale Überprüfung von Variations-Quantenkreisen 变量量电路的正式核查 2507.10635v1

Authors (4): Nicola Assolini, Luca Marzari, Isabella Mastroeni, Alessandra di Pierro

Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms, offering a hybrid quantum-classical framework that, under certain aspects, can be considered similar to classical deep neural networks. A shared aspect is, for instance, their vulnerability to adversarial inputs, small perturbations that can lead to incorrect predictions. While formal verification techniques have been extensively developed for classical models, no comparable framework exists for certifying the robustness of VQCs. Here, we present the first in-depth theoretical and practical study of the formal verification problem for VQCs. Inspired by abstract interpretation methods used in deep learning, we analyze the applicability and limitations of interval-based reachability techniques in the quantum setting. We show that quantum-specific aspects, such as state normalization, introduce inter-variable dependencies that challenge existing approaches. We investigate these issues by introducing a novel semantic framework based on abstract interpretation, where the verification problem for VQCs can be formally defined, and its complexity analyzed. Finally, we demonstrate our approach on standard verification benchmarks.

变化量子电路(VQCs)是许多量子机器学习算法的核心组成部分,它提供了一个混合的量子古典框架,在某些方面可以被视为与古典的深神经网络类似。例如,一个共同的方面是,它们易受对抗性投入的影响,小扰动可能导致不正确的预测。虽然对古典模型已经广泛开发了正式的核查技术,但没有类似的框架来证明VQCs的稳健性。在这里,我们提出了对VQCs正式核查问题的首次深入的理论和实践研究。在深入学习中使用的抽象解释方法的启发下,我们分析了在量子环境中的间隔可达性技术的适用性和局限性。我们表明,量子特有的方面,例如国家正常化,引入了质疑现有方法的可变依赖性。我们根据抽象解释引入新的语法框架来调查这些问题,从而可以正式界定VQ的核查问题,并分析其复杂性。最后,我们展示了我们在标准核查基准上的方法。

Article 28

Title@2025-07-14 (1): ReDemon UI: Reactive Synthesis by Demonstration for Web UI

Title: ReDemon UI: Reactive Synthesis by Demonstration for Web UI ReDemon UI: Reaktive Synthese durch Demonstration für Web UI ReDemon UI: 网络 UI 演示的反活动合成 2507.10099v1

Authors (4): Jay Lee, Gyuhyeok Oh, Joongwon Ahn, Xiaokang Qiu

ReDemon UI synthesizes React applications from user demonstrations, enabling designers and non-expert programmers to create UIs that integrate with standard UI prototyping workflows. Users provide a static mockup sketch with event handler holes and demonstrate desired runtime behaviors by interacting with the rendered mockup and editing the sketch. ReDemon UI identifies reactive data and synthesizes a React program with correct state update logic. We utilize enumerative synthesis for simple UIs and LLMs for more complex UIs.

ReDemon 界面合成用户演示的适应应用程序,使设计师和非专家程序员能够创建与标准 UI 原型流程集成的UI 。用户提供静态模拟草图,带有事件处理器孔,并通过与完成的模型互动和编辑草图来显示理想运行时间行为。 ReDemon 界面识别反应数据,并合成一个符合正确状态更新逻辑的React程序。我们用数字合成来为简单的 UIS 和 LLMS 提供更复杂的 UIS 。

Article 29

Title@2025-07-14 (1): BeePL: Correct-by-compilation kernel extensions

Title: BeePL: Correct-by-compilation kernel extensions BeePL: Richtig-nach-Sammlung Kernel-Erweiterungen BEPL: 校正式编译内核扩展 2507.09883v1

Authors (7): Swarn Priya, Frédéric Besson, Connor Sughrue, Tim Steenvoorden, Jamie Fulford, Freek Verbeek, Binoy Ravindran

eBPF is a technology that allows developers to safely extend kernel functionality without modifying kernel source code or developing loadable kernel modules. Since the kernel governs critical system operations and enforces isolation boundaries between user space and privileged data, any mechanism that modifies its behavior must meet the highest standards of safety and correctness. To this end, the eBPF toolchain includes a verifier, which statically checks safety properties such as memory access validity, bounded loops, and type correctness before loading the program into the kernel. However, the existing verifier is both overly conservative in some cases-rejecting valid programs-and unsound in others, permitting unsafe behavior that violates the intended semantics of the kernel interface. To address these challenges, we introduce BeePL, a domain-specific language for eBPF with a formally verified type system. The BeePL type system, along with the language design, statically enforces key safety properties such as type-correct memory access, safe pointer usage, absence of unbounded loops, and structured control flow. These guarantees are backed by formal type soundness proofs, ensuring that well-typed programs satisfy the safety invariants required by the eBPF execution environment. BeePL also proves that well-typed source programs meet critical eBPF-specific properties related to memory safety, termination, and control flow, enabling high-level reasoning prior to compilation. For properties not fully enforceable statically-such as dynamic bounds and undefined behavior-BeePL inserts semantics-preserving runtime checks during compilation. We develop a verified compilation strategy that extends CompCert to generate BPF bytecode from BeePL programs, establishing a principled foundation for an end-to-end verifiable toolchain for safe kernel extensions.

eBPF 是一种技术,使开发者能够在不修改内核源代码或开发可装载内核模块的情况下安全扩展内核功能。 由于内核监管关键系统操作并强制实施用户空间和特许数据之间的隔离界限, 任何改变其行为的机制必须达到安全和正确性的最高标准。 为此, eBPF 工具链中包含一个校验器, 该校验器在将程序装入内核之前静态检查安全性能, 如内核存存存存存存取有效性、 约束循环和输入正确性等。 但是, 现有的核查器在某些情况中过度保守, 拒绝有效的程序, 在其它情况下则不响, 允许违反内核界面预设的语义的不安全行为。 为了应对这些挑战, 我们引入BPLPL, 一种特定域语言语言语言, 连同语言设计, 静态执行关键安全性安全性安全性, 安全性内存存数据, 安全性点使用, 缺少非内存循环, 以及结构化控制流程。 这些保证由正式的保密性 B型内存系统, 更新的内存系统, 运行前的内存系统, 运行的内存系统, 运行的内存系统, 运行的内存系统, 运行的内存系统, 运行的内存的内存的内存的内存程序, 运行的内存的内存的内存的内存的内存的内存的内核程序, 运行的内存程序, 运行的内存的内存的内存的内存的内存的内核程序, 运行的内存的内存的内核程序, 。

Article 30

Title@2025-07-13 (7): Oracular Programming: A Modular Foundation for Building LLM-Enabled Software

Title: Oracular Programming: A Modular Foundation for Building LLM-Enabled Software Orakuläre Programmierung: Modulare Grundlage für den Aufbau von LLM-fähiger Software 眼镜编程:建筑LLM-Enable软件模块基金会 2502.05310v2

Authors (2): Jonathan Laurent, André Platzer

Large Language Models have proven surprisingly effective at solving a wide range of tasks from just a handful of examples. However, their lack of reliability and modularity limits their capacity to tackle large problems that require many steps of reasoning. In response, researchers have proposed advanced pipelines that leverage domain-specific knowledge to chain smaller prompts, provide intermediate feedback and improve performance through search. However, the current complexity of writing, tuning, maintaining and improving such pipelines has limited their sophistication. We propose oracular programming, a foundational paradigm for building LLM-enabled applications that lets domain experts express high-level problem-solving strategies as programs with unresolved choice points. These choice points are resolved at runtime by LLMs, which generalize from user-provided examples of correct and incorrect decisions. An oracular program is composed of three orthogonal components: a strategy that consists in a nondeterministic program with choice points that can be reified into a search tree, a policy that specifies how to navigate this tree with the help of LLM oracles, and a set of demonstrations that describe successful and unsuccessful search tree navigation scenarios across diverse problem instances. Each component is expressed in a dedicated programming language and can be independently improved or substituted. We address the key programming language design challenges of modularly composing oracular programs and enforcing consistency between their components as they evolve.

大型语言模型在解决众多任务方面证明是出乎意料的,仅举几个例子即可证明如此。然而,它们缺乏可靠性和模块性限制了它们解决需要许多推理步骤的重大问题的能力。作为回应,研究人员建议了先进的管道,将特定领域知识用于连锁较小的提示,提供中间反馈,并通过搜索提高绩效。然而,目前书写、调试、维护和改进这些管道的复杂性限制了它们的精密性。我们提议了个性化的编程,这是建立LLLM驱动应用程序的基础范例,让域专家将高层次的解决问题战略作为有未解决的选择点的方案来表达。这些选择点由LMS在运行时解决,它从用户提供的正确和不正确决定的例子中概括。一个或特定的方案由三个或多层次的构件组成:包含非定性方案的战略,其选择点可以重新改成搜索树;我们提议了一种政策,规定如何用LM或触摸索法来引导这棵树,以及一套描述成功和不成功搜索树形导航情景的示范。每个构件都是由用户提供的正确和不正确和不正确决定性决定性决定,我们可以独立地在设计中独立地表达出其格式设计中进行。

Article 31

Title@2025-07-13 (7): Equality Saturation for Optimizing High-Level Julia IR

Title: Equality Saturation for Optimizing High-Level Julia IR Gleichstellungssättigung für die Optimierung von High-Level Julia IR 优化高级别Julia IR 平等饱和 2502.17075v2

Authors (3): Jules Merckx, Tim Besard, Bjorn De Sutter

Compilers are indispensable for transforming code written in high-level languages into performant machine code, but their general-purpose optimizations sometimes fall short. Domain experts might be aware of certain optimizations that the compiler is unable to apply or that are only valid in a particular domain. We have developed a system that allows domain experts to express rewrite rules to optimize code in the Julia programming language. Our system builds on e-graphs and equality saturation. It can apply optimizations in the presence of control flow and side effects. As Julia uses multiple dispatch, we allow users to constrain rewrite rules by argument types, and propagate type information through the e-graph representation. We propose an ILP formulation for optimal e-graph extraction taking into account dominance properties for code reuse and introduce CFG skeleton relaxation to rewrite calls to pure functions as well as those with side effects. Use cases demonstrate that our system can perform rewrites on high-level, domain-specific code, as well as on lower-level code such as Julia’s broadcasting mechanism. Finally, we analyze the required compilation time.

编译器对于将高语言的代码转换为性能机器代码是不可或缺的,但是它们的通用优化有时是不足的。 域专家可能知道编译器无法应用或仅在特定领域有效的某些优化。 我们开发了一个系统,让域专家表达重写规则以优化朱丽亚编程语言的代码。 我们的系统建立在电子绘图和平等饱和的基础上。 它可以在控制流和副作用的情况下应用优化。 朱丽亚使用多种发送方式, 我们允许用户通过参数类型限制重写规则, 通过电子图表代表方式传播类型信息。 我们建议了一种ILP 格式, 用于最佳电子制图提取, 以考虑到代码再利用的主导特性, 并引入 CFG 骨架松动, 以重写纯功能的呼声以及具有副作用的呼声。 使用案例表明, 我们的系统可以在高层次、 特定域代码上进行重写, 以及像 Julia 广播机制那样的低级别代码上进行重写。 最后, 我们分析了所需的编译时间 。

Article 32

Title@2025-07-13 (7): Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams

Title: Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams Gebundenes Modell Überprüfung von RISC-V-Maschinencode mit Kontext-Frei-Sprache bestellt binären Entscheidungsdiagrammen RISC-V型机器编码与无环境-无语言有秩序二进制决定图的对RISC-V型机器编码的边界模式检查 2507.09539v1

Authors (4): Anna Bolotina, Christoph M. Kirsch, Stefanie Muroya Lei, Matthias Pleschinger

Symbolic execution is a powerful technique for analyzing the behavior of software yet scalability remains a challenge due to state explosion in control and data flow. Existing tools typically aim at managing control flow internally, often at the expense of completeness, while offloading reasoning over data flow to SMT solvers. Moreover, reasoning typically happens on source code or intermediate representation level to leverage structural information, making machine code generation part of the trust base. We are interested in changing the equation in two non-trivial ways: pushing reasoning down to machine code level, and then offloading reasoning entirely into SMT solvers and other, possibly more efficient solver technology. In more abstract terms, we are asking if bit-precise reasoning technology can be made scalable on software, and not just hardware. For this purpose, we developed two tools called rotor and bitme for model generation and bounded model checking, respectively. We chose RISC-V restricted to integer arithmetic as modeling target for rotor since RISC-V integer semantics is essentially equivalent to established SMT semantics over bitvectors and arrays of bitvectors. While state-of-the-art SMT solvers struggle in our experiments, we have evidence that there is potential for improvement. To show the potential, we have slightly generalized and then implemented in bitme two types of binary decision diagrams (BDDs): algebraic decision diagrams (ADDs) and context-free-language ordered binary decision diagrams (CFLOBDDs). Bitme uses BDDs to propagate program input through models, essentially generalizing constant propagation to domain propagation. SMT solvers only get involved when model input cannot be propagated, significanly speeding up SMT solving. We then study the impact on state explosion of CFLOBDDs, which are potentially more scalable than ADDs.

分析软件行为的方法非常有力, 但它的可缩放性仍是一个挑战。 现有工具通常旨在管理内部控制流程, 通常以完整性为代价, 而将数据流的推理卸到 SMT 解答器。 此外, 推理通常发生在源代码或中间代表级别上, 以利用结构信息, 使机器代码生成成为信任基础的一部分。 我们有意以两种非三进制方式改变方程式: 将推推到机器代码级别, 然后将推离完全装入 SMT 解解析器和其他( 可能更有效率的求解器技术 ) 。 在更抽象的术语中, 我们问, 是否可以将百分解推推推理推理推理技术在软件上进行缩, 而不只是硬件。 为此, 我们开发了两种工具, 分别称为模型生成和绑定模式的转盘和比重检查。 我们选择了 RISC- V 定序的算法, 从本质上来说, 将SMT 解算法比特的解解解和比特数字直径直径直径直径直径直径直径直径推, , , 的算法的解解解的解解解解路路路基路路路路标的变变变变。

Article 33

Title@2025-07-13 (7): PHOENIX: Pauli-Based High-Level Optimization Engine for Instruction Execution on NISQ Devices

Title: PHOENIX: Pauli-Based High-Level Optimization Engine for Instruction Execution on NISQ Devices PHOENIX: Pauli-basierte High-Level-Optimierungs-Engine zur Instruction Execution auf NISQ-Geräten PHOENIX: 以保利为基础的高级优化引擎,用于NISQ设备指令执行 2504.03529v5

Authors (5): Zhaohui Yang, Dawei Ding, Chenghong Zhu, Jianxin Chen, Yuan Xie

Variational quantum algorithms (VQA) based on Hamiltonian simulation represent a specialized class of quantum programs well-suited for near-term quantum computing applications due to its modest resource requirements in terms of qubits and circuit depth. Unlike the conventional single-qubit (1Q) and two-qubit (2Q) gate sequence representation, Hamiltonian simulation programs are essentially composed of disciplined subroutines known as Pauli exponentiations (Pauli strings with coefficients) that are variably arranged. To capitalize on these distinct program features, this study introduces PHOENIX, a highly effective compilation framework that primarily operates at the high-level Pauli-based intermediate representation (IR) for generic Hamiltonian simulation programs. PHOENIX exploits global program optimization opportunities to the greatest extent, compared to existing SOTA methods despite some of them also utilizing similar IRs. Experimental results demonstrate that PHOENIX outperforms SOTA VQA compilers across diverse program categories, backend ISAs, and hardware topologies.

以汉密尔顿模拟为基础的量子变量算法(VQA)代表了专门一类量子程序,由于Qbits和电路深度方面的资源需求有限,适合近期的量子计算应用。与传统的单平方位(1Q)和2平方位(2Q)门序列代表法不同,汉密尔顿模拟程序基本上由被称为Pauli Expententiations(保利字符串加系数)的有纪律的子例程组成,这些子程程由不同的安排组成。为了利用这些不同的程序特点,本研究引入了PHOENIX,这是一个非常有效的汇编框架,主要在基于保利的高级中间代表制中用于普通汉密尔顿模拟程序。PHOENIX利用了全球方案优化机会,而与现有的SOTA方法相比,尽管其中一些方法也使用类似的IRs。实验结果表明,PHENIX超越了不同程序类别、后端ISA和硬件表的SOTA VQA编集器。

Article 34

Title@2025-07-11 (5): Semantic Source Code Segmentation using Small and Large Language Models

Title: Semantic Source Code Segmentation using Small and Large Language Models Semantische Quellcode-Segmentierung mit kleinen und großen Sprachmodellen 使用小型和大语言模式的语义源代码代码分割 2507.08992v1

Authors (5): Abdelhalim Dahou, Ansgar Scherp, Sebastian Kurten, Brigitte Mathiak, Madhu Chauhan

Source code segmentation, dividing code into functionally coherent segments, is crucial for knowledge retrieval and maintenance in software development. While enabling efficient navigation and comprehension of large codebases, manual and syntactic analysis approaches have become impractical as repositories grow, especially for low-resource languages like R and their research domains (e.g., social sciences, psychology).This paper introduces an automated, domain-specific approach for research R code segmentation using Large and Small Language Models (LLMs/SLMs). It presents two novel approaches and a human-annotated dataset, StatCodeSeg. We explore two distinct approaches: line-by-line analysis with context and range-based segment determination. We experiment with LLMs and fine-tuned SLMs. To support the generalizability of our approaches, we also include experiments on Python code from the computer science domain.Our results show that context-based line-by-line analysis is superior over range-based segmentation.Using smaller language models like CodeBERT and an encoder-only version of CodeT5+ are better than their LLM counterparts. Most notably, these two best-performing models did not see R code during pre-training versus the LLMs but were only fine-tuned on 4,130 lines of manually annotated code.

源代码分割法将代码分为功能一致部分,对于软件开发方面的知识检索和维护至关重要。虽然随着库库的成长,特别是R及其研究领域(例如社会科学、心理学)等低资源语言的储存库的成长,能够有效地导航和理解大型代码库,人工和合成分析方法变得不切实际,特别是对于R及其研究领域(例如社会科学、心理学)等低资源语言而言更是如此。本文介绍了使用大语言和小语言模型(LLLMS/SLMS)进行的研究代码分割的自动、具体领域的方法。它提出了两种新颖的方法和一个带有人文注释的数据集,StatCCodeSeg。我们探索了两种不同的方法:逐行分析,同时根据背景和基于范围确定部分。我们试验LLMSM和经过精细调整的可持续土地管理方法。为了支持我们的方法的通用性,我们还将包括计算机科学领域的Python代码实验。我们的研究结果表明,基于背景的逐行分析比基于范围的分割法的分解法更为优越。我们发现,像CBERT5+只编码的编码版本比LLMM4号前改进了。

Article 35

Title@2025-07-11 (5): Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny

Title: Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny Können große Sprachmodelle den Studierenden helfen, Software-Korrektur zu beweisen? Eine experimentelle Studie mit Dafny 大语言模型能帮助学生证明软件正确性吗? 与Dafny的实验研究 2506.22370v3

Authors (4): Carolina Carreira, Álvaro Silva, Alexandre Abreu, Alexandra Mendes

Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness, by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master’s students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface that logged all interactions, and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning rather than substitution.

然而,LLMS在支持认知要求高的任务(如计算程序核查)方面的作用仍然不为人所知。本文调查了学生在解决Dafny的正式核查练习时如何与LLM互动。 Dafny是支持功能正确性的一种语言,它使程序设计员能够编写正式的规格,并自动核实执行符合规格。我们与注册参加正规方法课程的硕士学生进行了混合方法研究。每个参与者都完成了两个核查问题,一个是能够使用记录所有互动的CatGPT用户界面,另一个是没有。我们确定了成功学生使用的战略,并评估了LLMS学生的信任程度。我们的调查结果显示,学生在使用CatGPT时表现得更好;然而,成绩与及时的质量挂钩。我们最后提出了将LMS更有效地纳入正规方法课程的实用建议,包括设计LMM-aware挑战,促进学习而不是替代。

Article 36

Title@2025-07-11 (5): Filter Equivariant Functions: A symmetric account of length-general extrapolation on lists

Title: Filter Equivariant Functions: A symmetric account of length-general extrapolation on lists Filter Equivariant Funktionen: Eine symmetrische Darstellung der Längen-allgemeinen Extrapolation auf Listen 过滤器等同函数 : 列表中长度一般外推法的对称账户 2507.08796v1

Authors (6): Owen Lewis, Neil Ghani, Andrew Dudzik, Christos Perivolaropoulos, Razvan Pascanu, Petar Veličković

What should a function that extrapolates beyond known input/output examples look like? This is a tricky question to answer in general, as any function matching the outputs on those examples can in principle be a correct extrapolant. We argue that a “good” extrapolant should follow certain kinds of rules, and here we study a particularly appealing criterion for rule-following in list functions: that the function should behave predictably even when certain elements are removed. In functional programming, a standard way to express such removal operations is by using a filter function. Accordingly, our paper introduces a new semantic class of functions – the filter equivariant functions. We show that this class contains interesting examples, prove some basic theorems about it, and relate it to the well-known class of map equivariant functions. We also present a geometric account of filter equivariants, showing how they correspond naturally to certain simplicial structures. Our highlight result is the amalgamation algorithm, which constructs any filter-equivariant function’s output by first studying how it behaves on sublists of the input, in a way that extrapolates perfectly.

超越已知输入/ 输出示例外推的函数应该像什么? 这是一个需要解答的棘手问题, 因为在那些示例上匹配输出的函数原则上可以是一个正确的外推法。 我们争论说, 一个“ 好” 外推法应该遵循某些类型的规则, 而我们在这里研究一个在列表函数中遵循规则特别具有吸引力的标准 : 该函数应该表现得可以预测, 即使某些元素被删除 。 在功能编程中, 表达这种清除操作的标准方式是使用过滤功能。 因此, 我们的文件会引入一个新的函数的语义类别 – – 过滤等同功能。 我们显示, 这个类包含一些有趣的实例, 证明一些基本的参数, 并将它与众所周知的地图等同功能类别联系起来 。 我们还展示了一个过滤电子等变量的几何描述, 显示它们如何自然地与某些简化结构相匹配 。 我们的突出结果就是混和算法, 它通过首先研究输入子列表中如何表现, 从而完美地表达出任何过滤- 等函数的输出 。

Article 37

Title@2025-07-11 (5): CCR 2.0: High-level Reasoning for Conditional Refinements

Title: CCR 2.0: High-level Reasoning for Conditional Refinements CCR 2.0: Hochrangige Begründung für bedingte Veredelungen CCR 2.0: 有条件改进的高层次理由 2507.04298v2

Authors (2): Youngju Song, Minki Cho

In recent years, great progress has been made in the field of formal verification for low-level systems. Many of them are based on one of two popular approaches: refinement or unary separation logic. These two approaches are very different in nature and offer complementary benefits in compositionality. Recently, to fuse these benefits into a single unified mechanism, a new approach called Conditional Contextual Refinement (CCR 1.0 for short) was proposed. In this paper, we advance CCR 1.0 and provide novel and intuitive reasoning principles, resulting in CCR 2.0. Achieving this goal was challenging due to non-trivial counterexamples which necessitated elegant changes to the model of CCR 1.0. On top of CCR 2.0, we show how to fuse the benefits of refinement, unary separation logic, and also relational separation logic. Our results are formalized in Rocq.

近年来,在对低级系统进行正式核查方面取得了巨大进展,其中许多是基于两种流行方法之一:改进或单一分离逻辑。这两种方法性质大不相同,在组成性方面具有互补性。最近,将这些效益整合为一个单一的统一机制,即所谓的有条件环境改进(CCCR 1.0用于简短的)的新办法。在本文件中,我们推进了CCR 1.0,提供了新颖和直观的推理原则,产生了CCCR 2.0。由于非三相反抽样,需要优雅地修改CCR 1.0模式,因此实现这一目标具有挑战性。在CCR 2.0的基础上,我们展示了如何整合完善、单一分离逻辑和关联分离逻辑的好处。我们在罗克正式确定了我们的结果。

Article 38

Title@2025-07-11 (5): Heterogeneous Dynamic Logic: Provability Modulo Program Theories

Title: Heterogeneous Dynamic Logic: Provability Modulo Program Theories Heterogene dynamische Logik: Wahrscheinlichkeit Modulo-Programm Theorien 变异动态逻辑:可变莫杜洛方案理论 2507.08581v1

Authors (4): Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert

Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be flexibly combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: Lifting extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and Combination enables cross-language reasoning in a single modality via Heterogeneous Dynamic Theories, facilitating the reuse of existing proof infrastructure. We formalize dynamic theories, their lifting and combination in Isabelle, and prove the soundness of all proof rules. We also prove relative completeness theorems for lifting and combination: Under common assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the “data theory”). We demonstrate HDL’s utility by verifying an automotive case study in which a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).

正式( 更不用说核实) 涉及多种编程语言的系统属性本质上具有挑战性。 我们引入了异质动态逻辑( HDL) , 将不同(动态)程序逻辑的推理原则与不同的(动态)程序逻辑( HDL) 相结合的框架。 HDL 反映了可讽刺性模版理论( SMT) 的架构: 个体动态逻辑及其计算法被视作动态理论,可以灵活地与使用不同程序逻辑校验的混合系统各组成部分的理由结合起来。 HDL 提供了两个关键操作: 提升个人动态理论,采用新的程序结构( 例如, 破坏操作或常规程序) , 并自动用新结构的正确推理原则来强化其计算; 合并使跨语言推理能够以单一的方式通过 Hetergenous 动态理论理论( Smodividiculate) , 便利现有证据基础设施的再利用。 我们将动态理论、 提升和组合在伊莎贝尔模式中证明所有证据规则的正确性。 我们还证明, 提高和组合理论的相对完整性: 在共同假设下, 解算法或组合理论的逻辑的逻辑中, 更难于动态逻辑中, 一种动态逻辑的动态逻辑学 。

Article 39

Title@2025-07-11 (5): SecRef: Securely Sharing Mutable References Between Verified and Unverified Code in F

Title: SecRef: Securely Sharing Mutable References Between Verified and Unverified Code in F SecRef: Sicheres Teilen von mutierbaren Referenzen zwischen verifiziertem und ungeprüftem Code in F SecRef:F中经核实的守则与未经核实的守则之间安全分享可窃取的参考文献 2503.00404v2

Authors (7): Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter

We introduce SecRef, a secure compilation framework protecting stateful programs verified in F against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we propose a way of tracking which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F* that this strategy ensures sound and secure interoperability with unverified code. Since SecRef* is built on top of the Monotonic State effect of F, these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.

我们引入了SecRef* 安全汇编框架, 保护F* 中核查的有条不紊的程序, 使其不受未经核实的编码的链接。 为了方便此设置的程序核查, 我们建议一种方法, 跟踪哪些参考与未经核实的编码共享,哪些不可共享, 其内容在调用未经核实的编码后也因此保证保持不变。 这种非共享引用的普遍属性, 在被核实的程序在调用到未经核实的编码时可以依赖的接口中暴露出来。 其余的改进类型以及未经核实的编码所期望的未经核实的编码预设和后条件, 被转换成关于共同引用的动态检查。 在F* 中, 我们正式证明, 该战略确保了与未经核实的编码之间的健全和安全互操作性。 由于SecRef* 是在F* 的单调国家效应顶端建的, 这些证据依赖于该效果的首个元表示方式, 这也是我们工作的一种贡献, 可以独立的兴趣。 最后, 我们使用SecRef* 与未经核实的简单合作时间表进行互动, 安全地与未经核实的细化。

Article 40

Title@2025-07-11 (5): EOLANG and $\varphi$-calculus

Title: EOLANG and $\varphi$-calculus EOLANG und $\varphi$-Berechnung EOLANG 和 美元计算法 2111.13384v6

Authors (1): Yegor Bugayenko

Object-oriented programming (OOP) is one of the most popular paradigms used for building software systems. However, despite its industrial and academic popularity, OOP is still missing a formal apparatus similar to $\lambda$-calculus, which functional programming is based on. There were a number of attempts to formalize OOP, but none of them managed to cover all the features available in modern OO programming languages, such as C++ or Java. We have made yet another attempt and created $\varphi$-calculus. We also created EOLANG (also called EO), an experimental programming language based on $\varphi$-calculus.

面向目标的编程(OOP)是用于建立软件系统的最受欢迎的范例之一,然而,尽管OOP在工业和学术上很受欢迎,但仍然缺少类似于美元计算的正式装置,而美元计算是功能性编程的基础。曾几次尝试将OOP正式化,但其中没有任何一次尝试能够涵盖现代OO编程语言的所有功能,如C++或Java。我们又尝试并创建了美元计算器。我们还创建了EOLANG(也称为EO),这是一种实验性编程语言,以美元计算。

Article 41

Title@2025-07-11 (5): Abstraction Functions as Types

Title: Abstraction Functions as Types Abstraktionsfunktionen als Typen 抽象函数类型 2502.20496v2

Authors (3): Harrison Grodin, Runming Li, Robert Harper

Software development depends on the use of libraries whose specifications constrain the client’s code and impose obligations on the implementation. It follows that any approach to verification at scale must also be modular, while permitting specification of both behavior and cost. Hoare’s notion of an abstraction function provides an elegant and effective methodology for such verifications, separating the implementation from the abstraction, and using an abstraction function to demonstrate the behavioral correctness of the former relative to the latter. For all of its influence, much of the Hoare methodology remains informal in that it relies on conventional separation between implementation and abstraction, and provides no linguistic support for ensuring that these conventions are obeyed. The purpose of this paper is to propose a synthetic account of Hoare’s methodology within univalent dependent type theory based on the principle that all types have abstract and concrete aspects by regarding abstraction functions as types, and thus enjoy the full range of typing constructs found in dependent type theory. Achieving this relies crucially on the notion of a phase distinction in type theory which gives rise to modalities that isolate, or fracture, a type into its concrete and abstract parts, and that permit the definition of a type given these aspects using a technique called gluing. Moreover, this approach scales to permit the specification and verification of the cost of programs, as well as their behavior, allowing clients to verify their own cost relative to these specifications and permit the implementor to realize them with tighter bounds. The resulting theory supports modular development of programs and proofs in a manner that hides technical details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.

软件开发取决于图书馆的使用情况,图书馆的规格限制客户的代码,并对执行过程规定了义务。因此,任何规模核查方法都必须是模块化的,同时允许对行为和成本做出规定。Haare的抽象功能概念为这种核查提供了一个优雅而有效的方法,将执行与抽象区分开来,并使用抽象功能来显示前者相对于后者的行为正确性。对于它的所有影响来说,许多Haare方法仍然是非正式的,因为它依赖于执行和抽象之间的常规区分,没有提供语言支持,以确保这些公约得到遵守。本文的目的是根据所有类型的抽象功能都具有抽象和具体方面作为抽象功能的原则,在单一的、依赖型型号的理论中提出Hoare方法的合成说明,并以此为基础,将Hooare方法的精密性纳入单项和抽象的规格中。实现这种分类概念的关键在于在类型理论理论中产生分离或断裂,在具体和抽象部分中不提供语言支持,并且允许将某种类型程序的精细度定义纳入其精确的规格,同时以精确的精确的精确的精确的规格来,使客户的精确的精确的核查方法得以实现其精确的规格,从而实现其精确的规格。

Article 42

Title@2025-07-10 (4): Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)

Title: Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version) Denotationale Semantik der graduellen Typisierung mittels Synthetischer Domänen-Theorie (Erweiterte Version) 使用合成保护域域理论(扩展版本)逐步打字的注解性语义表达式 2411.12822v2

Authors (3): Eric Giovannini, Tingting Ding, Max S. New

Gradually typed programming languages, which allow for soundly mixing static and dynamically typed programming styles, present a strong challenge for metatheorists. Even the simplest sound gradually typed languages feature at least recursion and errors, with realistic languages featuring furthermore runtime allocation of memory locations and dynamic type tags. Further, the desired metatheoretic properties of gradually typed languages have become increasingly sophisticated: validity of type-based equational reasoning as well as the relational property known as graduality. Many recent works have tackled verifying these properties, but the resulting mathematical developments are highly repetitive and tedious, with few reusable theorems persisting across different developments. In this work, we present a new denotational semantics for gradual typing developed using guarded domain theory. Guarded domain theory combines the generality of step-indexed logical relations for modeling advanced programming features with the modularity and reusability of denotational semantics. We demonstrate the feasibility of this approach with a model of a simple gradually typed lambda calculus and prove the validity of beta-eta equality and the graduality theorem for the denotational model. This model should provide the basis for a reusable mathematical theory of gradually typed program semantics. Finally, we have mechanized most of the core theorems of our development in Guarded Cubical Agda, a recent extension of Agda with support for the guarded recursive constructions we use.

渐进式编程语言可以将静态和动态键入式编程风格进行合理混合,对元神话学家来说,这是一个巨大的挑战。即使最简单且逐步打字的语言至少具有递转和错误的特点,即使最简单且逐渐打字的语言也至少具有递归和错误的特点,而现实语言则具有更多的记忆位置和动态类型标记的运行时间分配。此外,逐渐打字的语言所希望的元理论特性也变得越来越复杂:基于类型方程推理的有效性以及被称为渐进式的关联属性。许多最近的工作已经解决了核实这些属性的问题,但由此产生的数学发展是高度重复和乏味的,在各个不同发展动态中很少有可重复的理论。在这项工作中,我们提出了一个新的代名词性词性词性词性词性词性词性,用保密域理论理论来逐步进行打字,将进步的逻辑关系与高级编程的模块性和可重复性属性属性属性属性属性特性结合起来。我们用一个简单的逐步打印的羊排加加糖化的模型来证明这一方法的可行性,并且证明比喻- 等式平等性和最渐进式的数学模型的升级性模型应该用来提供最终的模型。

Article 43

Title@2025-07-10 (4): QCP: A Practical Separation Logic-based C Program Verification Tool

Title: QCP: A Practical Separation Logic-based C Program Verification Tool QCP: Eine praktische Trennung Logisch-basiertes C-Programm Verifikationswerkzeug QCP:基于实际隔离逻辑的C方案核查工具 2505.12878v2

Authors (13): Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao

As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, there still remain %these tools still continue to encounter substantial difficulties when applying these tools to complex, real-world scenarios. To address these difficulties, this paper introduces a novel verification tool, called \textbf{Qualified C Programming Verifier (QCP)}. QCP incorporates a refined front-end %syntax of assertion language to enhance user interaction. The proposed assertion language aims to %syntax is designed to lower the entry barrier for verification tools, improve proof efficiency by improving automation, and facilitate a deeper understanding of both the program and its verification results.

随着软件系统规模和复杂性的急剧扩大,确保其正确性、安全和可靠性成为日益艰巨的挑战。尽管在核查技术和工具方面有了显著的进步,但是仍然有%这些工具在将这些工具应用于复杂的现实世界情景方面仍然面临着巨大的困难。为了解决这些困难,本文件引入了一种新型的核查工具,称为\ textb-ZQATIC(QCP)}。QCP采用了一种精细的前端 %syngycast 语言,以加强用户的互动。拟议的主张语言旨在使用 %syngyx,目的是降低核查工具的进入屏障,通过改进自动化提高证明效率,并促进对程序及其核查结果的更深入了解。

Article 44

Title@2025-07-10 (4): Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)

Title: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version) Modulare Begründung über Fehlergrenzen für gleichzeitige probabilistische Programme (Erweiterte Version) 用于同时概率程序(例外版本)的错误误界的模块原因 2503.04512v2

Authors (6): Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity. Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework

我们提出了第一个更高顺序的共和分离逻辑Coneris, 这是关于更高顺序同时概率程序与较高顺序状态的较高顺序同时概率程序误差概率界限的推理的首个更高顺序共和分离逻辑。 为了支持关于同时(非概率)程序模块的模块推理, 最先进的程序逻辑通过逻辑原子概念将典型的线性概念内化了逻辑内线性概念。 共和逻辑将这一理念扩展至概率共和程序模块。 因此, 共和逻辑通过在逻辑中捕捉随机化逻辑原子的新概念来支持概率共和模块的模块推理。 为了做到这一点, Coneris使用预取样磁带和新颖的概率更新模式来描述线性点的概率变化。 我们通过较小的合成实例和较大的案例研究来展示这一方法。 所提出的所有结果,包括元理论,已经在罗克证据助理和伊里斯分离逻辑框架中被机械化。

Article 45

Title@2025-07-10 (4): On Propositional Program Equivalence (extended abstract)

Title: On Propositional Program Equivalence (extended abstract) Über Propositionelle Programmäquivalenz (erweiterte Zusammenfassung) 提议方案等效(扩展抽象) 2507.07480v1

Authors (1): Tobias Kappé

General program equivalence is undecidable. However, if we abstract away the semantics of statements, then this problem becomes not just decidable, but practically feasible. For instance, a program of the form “if $b$ then $e$ else $f$” should be equivalent to “if not $b$ then $f$ else $e$” - no matter what $b$, $e$ and $f$ are. This kind of equivalence is known as propositional equivalence. In this extended abstract, we discuss recent developments in propositional program equivalence from the perspective of (Guarded) Kleene Algebra with Tests, or (G)KAT.

一般程序等值是不可变的。 但是, 如果我们抽象地删除语句的语义, 这个问题不仅可以分解, 而且实际上可行 。 例如, “ 如果一美元, 那么一美元, 另一美元” 形式的方案应该等同于“ 如果不是一美元, 那么一美元, 那么其他美元” 。 不论美元, 美元, 美元和美元。 这种等值被称为推论等值 。 在这个扩展的抽象中, 我们从( Kleene Algebra with Tests) 或 ( G) KAT 的角度讨论提议方案等值的最新发展 。