Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
安全编译最突出的形式化标准是完全抽象，保持和反映上下文等价。最近的工作介绍了鲁棒编译，定义为保持超属性的鲁棒满足，即，他们对任意攻击者的满意度。在本文中，我们首先比较了这两种安全编译方法。为此，我们提供了一个精确的描述的超性能，是强大的满足程序编译与一个完全抽象的编译器，并表明它们可以是无意义的或平凡的。然后，我们提出了一个新的标准制定的数学操作语义（MOS）的框架内的安全编译，保证充分的抽象和保存的强大的满足超属性在一个更明智的方式。
2021-09-20 cs.CR cs.PL
Structural Resolution for Abstract Compilation of Object-Oriented Languages
我们提出了基于共归纳逻辑编程的面向对象语言的精确静态类型分析的抽象编译。源代码被翻译成一个逻辑程序，然后类型检查和推理问题就变成了要解决的关于结果逻辑程序的查询。我们利用共归纳语义来处理递归类型和方法产生的无限项和证明。由于最近的概念，结构解析共归纳逻辑编程，我们能够推断出非常精确的类型信息，包括一类不合理的递归类型，导致非终止先前考虑共归纳语义。我们还展示了如何转换逻辑程序，使它们满足结构归结的操作语义的先决条件，我们证明了这一步骤不影响的语义的逻辑程序。
2017-09-14 cs.PL
Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)
我们映射的空间的可靠性标准的安全编译的基础上，在任意对抗性的情况下，我们称之为强大的超属性保存的超属性保存。为此，我们研究了几类超属性的保留，并为每个类提出了安全编译的等效“无属性”特征，通常更适合于证明。即使是我们最强的健全性标准，所有超属性的鲁棒保存，似乎可以实现简单的转换和证明使用上下文回翻译技术以前开发的显示完全抽象的编译。虽然证明不安全的超属性的鲁棒保存需要这种强大的上下文反向翻译技术，但为了鲁棒地保存安全超属性，将每个有限迹前缀翻译回源上下文似乎就足够了。
2017-12-20 cs.CR cs.PL
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
安全编译可以防止对编译代码的所有低级攻击，并允许对源语言的安全性进行合理的推理。在这项工作中，我们提出了一个新的攻击者模型的安全编译，扩展了众所周知的概念，充分的抽象，以确保保护相互不信任的组件。我们设计了一个编译器链（编译器，链接器和加载器）和一个新的安全监视器，共同抵御这种强大的攻击模型。该监视器是使用最近提出的，通用的基于标签的保护框架，称为微策略，它配备了硬件支持高效缓存和形式化验证方法。我们的监视器保护抽象的一个简单的面向对象的语言-类隔离，方法调用的纪律，和类型安全-对任意低级别的攻击者。
2015-10-02 cs.CR cs.PL
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Universidad Politécnica de Madrid（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
该研究提出算子语义与抽象编译框架，将其应用于静态代价分析，开发出支持通用函数未知量等的最优递归提取技术，提升了代价分析的可靠性与精确性。
2026-08-11 cs.LO cs.PL
Two-level Just-in-Time Compilation with One Interpreter and One Engine
运行Java或JavaScript的现代强大虚拟机支持多层JIT编译和优化功能，以实现其高性能。然而，实现和维护多个相互交互的编译器/优化器需要勤奋的VM开发人员。在本文中，我们提出了一种在RPython中实现两级JIT编译的技术，而无需从头开始实现多个解释器或编译器。作为初步实现，我们创建了自适应RPython，它可以执行基于线程代码的基线JIT编译和跟踪JIT编译。我们还用它实现了一个小型的程序设计语言。此外，我们初步评估了该小型语言的性能，我们的基线JIT编译运行速度比仅解释器执行快1.77倍。此外，我们观察到，当我们为不同的目标方法应用最佳JIT编译时，性能与优化JIT编译策略的性能基本相同，节省了大约40%的编译代码大小。
2022-01-23 cs.PL
Modular, Fully-abstract Compilation by Approximate Back-translation
本文提出通过近似反向翻译技术，解决源语言表达能力不足时编译器完全抽象性证明的难题，并在STLC到ULC编译器上实现首个Coq机械化证明。
2017-10-24 cs.PL
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)
我们提出了一个新的安全编译的正式标准，提供了强大的安全保证组件编写的不安全，低级语言与C风格的未定义行为。我们的标准超越了最近的建议，保护跟踪属性的一个单一的组件对敌对的情况下，在一个系统中的相互不信任的组件模型动态妥协。每个组件都受到保护，不受所有其他组件的影响，直到它接收到触发未定义行为的输入，导致它受到损害并攻击其余未受损害的组件。为了说明这个模型，我们展示了一个安全的编译链，一个不安全的语言与缓冲区，程序和组件，编译成一个简单的RISC抽象机与内置的划分。这个抽象机器提供的保护保证可以在机器代码级别使用软件故障隔离或基于标记的引用监控来实现。我们正在进行机器检查证明，表明这个编译器满足我们的安全编译标准。
2017-10-31 cs.CR cs.PL
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
（这是为了适应阿尔十四愚蠢的限制。请参阅PDF以获取完整摘要。）我们是第一个彻底探索基于鲁棒属性保护的正式安全编译标准的大空间，即，在任意对抗性上下文中保持满足的属性。我们研究鲁棒地保持各种类别的跟踪属性，如安全，超性质，如不干扰，和关系超性质，如跟踪等价。这导致了许多新的安全编译标准，其中一些比完全抽象更容易实现和证明，其中一些提供了严格的更强的安全保证。对于每一个研究的标准，我们提出了一个等效的“无属性”的表征，澄清证明技术适用。对于关系属性和超属性，它涉及多个程序的行为，我们的正式定义的属性类本身是新颖的。我们将我们的标准，其相对强度，并显示几个崩溃和分离的结果。最后，我们适应现有的证明技术表明，即使是最强的安全编译标准，所有关系hyperproperties的鲁棒保存，是可以实现的一个简单的翻译从静态类型到动态类型的语言。
2019-05-17 cs.CR cs.PL
An Improved Proof-Theoretic Compilation of Logic Programs
在以前的工作中，我们表明，逻辑编程编译可以给出一个通用的抽象逻辑程序设计语言的证明理论的理由，并证明了这种技术的情况下，遗传Harrop公式及其线性变体。编译后的子句本身就是逻辑公式，除了在与它们的头相匹配的原子目标上存在二阶抽象。在本文中，我们重新审视我们以前的结果，以更详细和更充分的逻辑理由，消除这种虚假的抽象。然后，我们改进所得到的技术，以有效地支持模式良好的程序。
2012-10-05 cs.LO cs.PL
Reading AI Model Compilation in MLIR Through the Lens of Formal Theories
Qualcomm Technologies International, Ltd.（高通国际有限公司）
本文通过形式理论（如项重写系统、精化演算、抽象解释）对应MLIR的匹配-重写引擎、阶段降低和范围分析，论证形式概念有助于明确抽象完备性、理想设计及实际权衡。
2026-06-25 cs.PL
SparseTIR: Composable Abstractions for Sparse Compilation in Deep Learning
University of Washington（华盛顿大学）；Carnegie Mellon University（卡内基梅隆大学）；OctoML；Shanghai Jiao Tong University（上海交通大学）
稀疏张量正迅速成为现代深度学习工作负载的关键组成部分。然而，开发高性能稀疏运算符可能是困难和繁琐的，现有的供应商库无法满足新的运营商不断增长的需求。稀疏张量编译器简化了运算符的开发，但用于深度学习的高效稀疏编译仍然具有挑战性，因为单一稀疏格式无法最大限度地提高硬件效率，并且单次编译器无法跟上最新的硬件和系统进步。在本文中，我们观察到，解决这两个挑战的关键是利用组合格式和组合转换。我们提出了SparseTIR，这是一种稀疏张量编译抽象，为深度学习工作负载提供了可组合格式和可组合转换。SparseTIR在这些可组合组件上构建了一个搜索空间，用于性能调优。通过这些改进，SparseTIR在GPU上为单个运算符获得了与供应商库一致的性能加速：GNN运算符为1.20- 2.34倍，稀疏注意力运算符为1.05- 2.98倍，稀疏卷积运算符为0.56- 7.45倍。SparseTIR还将GraphSAGE训练的端到端GNN加速了1.08- 1.52倍，RGCN推理加速了4.20- 40.18倍。
2023-02-21 cs.AI cs.LG cs.PL
Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
在最近的工作中，我们已经展示了如何通过将程序抽象编译成Horn公式f来为面向对象语言定义非常精确的类型系统。那么类型推断就等于解决了一个特定的目标。f的共归纳（也就是最大的）Herbrand模型。以这种方式定义的类型系统是理想化的，因为在最有趣的实例化中，共同归纳的Herbrand论域和目标导子的项都不能被直接表示。然而，声音和相当有表现力的近似可以通过只考虑正则项和导数来实现。在这样做的时候，引入一个适当的子类型关系来形式化类型之间近似的概念是至关重要的。本文研究了建立在联合和对象类型构造函数上的共归纳项的子类型关系。我们定义了一个解释的类型作为一组值引起的一个相当直观的关系的成员资格的值类型，并证明了子类型的定义是健全的w.r.t.类型解释之间的子集包含。可靠性的证明使我们能够简化压缩派生的概念，并发现先前给出的子类型定义并没有涵盖空类型的所有可能表示。
2010-06-08 cs.LO cs.PL
Contract-Aware Secure Compilation
微体系结构攻击利用指令集体系结构（ISA）与处理器实际执行指令的方式之间的抽象间隙来损害系统的机密性和完整性。为了保护系统免受微架构攻击，程序员需要对这些微架构副作用进行推理和编程。然而，我们不能也不应该期望程序员为特定的处理器及其安全保证手动定制程序。相反，我们可以依靠编译器（和安全编译社区），因为它们可以在弥合这一差距方面发挥重要作用：编译器应该针对特定的处理器微架构安全保证，并且应该利用这些保证来生成安全代码。为了实现这一目标，我们概述了合同感知安全通信（CASCO）的想法，其中编译器是参数相对于硬件/软件安全合同，抽象捕捉处理器的安全保证。也就是说，编译器将自动利用契约中形式化的保证，以确保程序级的安全属性在微体系结构级得到保留。
2020-12-28 cs.CR cs.PL
TWAM: A Certifying Abstract Machine for Logic Programs
类型保持（或类型化）编译使用类型化派生来证明编译的正确性。我们为Prolog的简单类型方言设计并实现了一个类型保留编译器，我们称之为T-Prolog。我们的方法的关键是一个新的认证抽象机，我们称之为类型沃伦抽象机（TWAM）。TWAM有一个足够强的依赖类型系统来指定逻辑框架LF中的逻辑程序的语义。我们提出了一个合理性元定理，它构成了部分正确性保证：良好类型的程序实现的逻辑程序指定的类型。这个元定理证明了我们的设计和实现的证明编译器从T-Prolog到TWAM。
2018-01-01 cs.LO cs.PL
Compositional Quantum Control Flow with Efficient Compilation in Qunity
本研究以Qunity语言为起点，提出高效编译高级量子控制流构造的方法，引入新抽象并实现完整编译器，通过多阶段优化技术大幅减少量子比特和门数量。
2025-09-03 cs.PL quant-ph
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
我们认为，功能性程序设计语言的编译器的实现和验证大大简化了采用高阶表示的语法称为高阶抽象语法或HOAS。HOAS的基本思想是使用一种元语言，它为绑定相关概念提供内置的逻辑处理。通过将元语言嵌入到更大的编程或推理框架中，可以将对象语言中的绑定结构的处理吸收到系统的元理论中，从而大大简化整体实现和推理过程。我们在这篇论文中提出并证明了上述论点的有效性的方法来验证执行的编译器转换的函数程序，利用HOAS。在这种方法中，函数程序的转换首先以基于规则的关系规范的形式表达。这些规范被渲染成语言lambda Prolog的程序。一方面，这些程序直接作为实现。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。lambda Prolog和Abella都支持使用HOAS方法。因此，它们构成了一个框架，可用于在验证编译中测试HOAS方法的好处。我们用它们来实现和验证一个编译器的代表性的功能程序设计语言，体现了许多编译器的核心，这些语言的转换。在这两个编程和推理阶段，我们展示了如何使用的HOAS方法显着简化了绑定结构的表示，操作，分析和推理。
2017-02-11 cs.LO cs.PL
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
我们提出了一个新的正式标准，用于评估不安全语言的安全编译方案，为遇到未定义行为（例如，访问越界数组）后可能受到损害的软件组件表达端到端的安全保证。我们的标准是第一个模型动态妥协的系统中相互不信任的组件，明确指定的特权。它阐明了应该如何保护每个组件不受其他组件的影响-特别是那些遇到未定义行为并受到损害的组件。每个组件都有安全编译保证-特别是，它的内部不变量受到保护，不受受损组件的影响-直到这个组件本身受到损害，之后我们假设攻击者可以完全控制并使用这个组件的特权来攻击其他组件。更准确地说，安全编译链必须确保动态受损的组件不能在目标级别破坏系统的安全属性，就像任意攻击者控制的组件（具有相同的接口和权限，但没有未定义的行为）在源级别已经可以破坏系统的安全属性一样。为了说明该模型，我们构建了一个安全的编译链的一个小的不安全的语言的缓冲区，程序和组件，针对一个简单的抽象机器内置的划分。我们给出了一个机器检查证明Coq，这个编译器满足我们的安全编译标准。最后，我们表明，分区抽象机提供的保护保证，可以实现在机器代码级别使用软件故障隔离或基于标签的参考监视器。
2019-11-29 cs.CR cs.PL
DyCL: Dynamic Neural Network Compilation Via Program Rewriting and Graph Optimization
UT Dallas（德克萨斯大学达拉斯分校）；UC Riverside（加州大学河滨分校）
DyCL 通过程序分析与变换将动态神经网络分解为多个无条件语句的子网络并独立编译，同时生成主机模块建模控制流，使现有 DL 编译器能以 100% 成功率编译 DyNNs，并获得 1.12 至 20.21 倍的性能提升。
2023-07-11 cs.CL cs.LG cs.PL
HUGR: A Quantum-Classical Intermediate Representation
本文提出HUGR，一种用于混合量子-经典程序的基于图的新型中间表示，具有高表达性和可扩展性，支持多抽象层次推理与模式匹配编译，并通过静态类型和线性量子类型保证安全性。
2025-10-13 cs.PL quant-ph
Dynamic Sparse Tensor Algebra Compilation
本文展示了如何生成高效的张量代数代码，计算动态稀疏张量，这些张量具有随时间演变的稀疏结构。我们提出了一种语言，精确地指定递归的，基于指针的数据结构，我们展示了这种语言可以表达广泛的动态数据结构，支持有效的修改，如链表，二叉搜索树和B树。然后，我们描述了在给定这种数据结构的高级规范的情况下，编译器可以如何生成代码以有效地对存储在上述数据结构中的动态稀疏张量进行覆盖和计算。此外，我们定义了一个抽象的接口，捕捉如何非零可以插入到动态数据结构，我们展示了这种抽象如何引导编译器发出有效的代码，存储稀疏张量代数计算的结果在动态数据结构。我们评估我们的技术，发现它产生高效的动态稀疏张量代数内核。我们的技术发出的代码计算PageRank算法的主要核心是1.05 $\times$一样快的Aspen，一个国家的最先进的动态图形处理框架。此外，我们的技术优于PAM，一个并行有序（键值）映射库，由7.40 $\times$时，用于实现元素的动态稀疏矩阵添加到一个静态稀疏矩阵。
2021-12-02 cs.MS cs.PL
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
本文提出SECOMP编译器，首次为主流语言C证明类似完全抽象的安全编译准则，将未定义行为限制在遭攻陷的分区内，并通过扩展CompCert及证明工程创新实现形式化安全编译。
2025-01-01 cs.CR cs.PL
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
诸如CHERI之类的能力机器提供可由编译器使用的存储器能力，以提供编译代码的安全益处（例如，记忆安全）。例如，现有的C到CHERI编译器通过遵循称为“指针即功能”（PAC）的原则来实现内存安全。非正式地，PAC说编译器应该将源语言指针表示为机器码能力。但是PAC编译器的安全属性还没有得到很好的理解。我们表明，内存安全只是一个方面，PAC编译器可以提供显着的额外的安全保证部分程序：编译器可以提供安全保证的编译单元，即使该编译单元后来被链接到攻击者提供的机器码。因此，本文是第一个正式研究部分程序PAC编译器的安全性。我们证明了这样的编译器的模型，它是完全抽象的。证明使用了一种新的证明技术（称为TrICL，读涓流），这应该是广泛的兴趣，因为它重用整个程序编译器的正确性关系的充分抽象，从而节省工作。我们还实现了我们的计划C CHERI，表明我们可以编译遗留的C代码，最小的变化，并表明编译代码的性能开销大致成正比的交叉编译单元函数调用的数量。
2021-05-04 cs.CR cs.PL
MappedTrace: Tracing Pointer Remotely with Compiler-generated Maps
Yale University（耶鲁大学）
MappedTrace利用编译器生成的只读映射远程精确识别程序快照中的指针，降低运行时开销，并支持内存泄漏检测与无限内存抽象等新应用。
2025-01-18 cs.CL cs.PL
The Program Hypergraph: Multi-Way Relational Structure for Geometric Algebra, Spatial Compute, and Physics-Aware Compilation
Braidpoint
提出程序超图（PHG）作为程序语义图的泛化，通过超边表示多重关系，解决空间数据流架构中的瓦片共置与路由约束以及几何代数计算中的分级多重积问题，实现几何正确性、内存布局、数值精度和硬件划分的联合推导。
2026-10-09 cs.AR cs.PL
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
本文提出一组基于语言的技术，在 F* 的 Low* 工具链中实现模块化高层验证与零开销低层代码生成，成功将 HACL* 扩展至十万行以上，并通用捕获流式 API 语义，修复了 Python 参考实现中的多个 CVE 漏洞。
2023-07-06 cs.PL
Unitary Expressions: A Necessary Abstraction for Extensible Quantum Programming Languages and Systems
针对量子计算软件生态中基于名称识别量子门易出错、难维护等问题，研究提出用函数式酉表达式表示法替代，推出含QGL语言、可微分即时编译器和QVM的OpenQudit系统，梯度计算速度领先，可提升量子编程系统的扩展性与易用性。
2025-01-16 cs.PL quant-ph
Trace-Relating Compiler Correctness and Secure Compilation
在最简单的形式中，编译器正确性被定义为将编译程序的跟踪集合包含到原始程序的跟踪集合中，这相当于保留所有跟踪属性。例如，这里的跟踪收集每次执行的外部可观察事件。然而，这个定义要求源语言和目标语言的踪迹集完全相同，而当语言相距很远或观察是细粒度的时，情况就不是这样了。为了克服这个问题，我们研究了一个广义的编译器的正确性定义，它使用源和目标的痕迹从潜在的不同的集合和连接的任意关系。我们开始了解什么保证这个广义的编译器正确性定义给我们的时候，实例化与非平凡的关系跟踪。当此跟踪关系不相等时，就不再可能保持源程序的跟踪属性不变。相反，我们提供了一个通用的表征的目标跟踪属性，确保正确编译一个程序，满足给定的源属性，和双重的源跟踪属性之一，需要显示，以获得一定的目标属性的编译代码。我们表明，这种观点编译器的正确性可以自然地占未定义的行为，资源枯竭，不同的源和目标值，侧通道，和各种抽象不匹配。最后，我们表明，同样的概括也适用于许多安全编译定义，其特征在于保护编译程序免受链接的对抗代码。
2020-02-23 cs.CR cs.PL
TensorIR: An Abstraction for Automatic Tensorized Program Optimization
Shanghai Jiao Tong University（上海交通大学）；Carnegie Mellon University（卡内基梅隆大学）；OctoML（OctoML公司）；University of Washington（华盛顿大学）；UC Berkeley（加州大学伯克利分校）；Amazon Web Services（亚马逊云科技）
在各种设备上部署深度学习模型已经成为一个重要的课题。硬件专业化的浪潮为多维张量计算带来了各种各样的加速原语。这些新的加速原语，以及新兴的机器学习模型，带来了巨大的工程挑战。在本文中，我们提出了TensorIR，一个编译器抽象优化程序与这些张量计算原语。TensorIR概括了现有机器学习编译器中使用的循环嵌套表示，将张量计算作为一等公民。最后，我们在我们的抽象之上构建了一个端到端框架，以自动优化给定张量计算原语的深度学习模型。实验结果表明，TensorIR编译自动使用给定硬件后端的张量计算原语，并提供与跨平台的最先进手动优化系统竞争的性能。
2022-10-27 cs.AI cs.LG cs.PL
Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs
该研究使用Isabelle/HOL验证了一个单遍编译器能够保持混合敏感并发程序的非干扰性，通过引入分解原则简化安全精化证明，并在真实用例上自动保留安全属性。
2022-02-28 cs.CR cs.LO cs.PL
Relax: Composable Abstractions for End-to-End Dynamic Machine Learning
Carnegie Mellon University（卡内基梅隆大学）；OpenAI；Shanghai Jiao Tong University（上海交通大学）；NVIDIA（英伟达）；University of Washington（华盛顿大学）；Hyperbolic；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；ByteDance（字节跳动）；Netflix（网飞）
本文提出编译器抽象Relax，通过跨层级统一表示与一等符号形状标注实现动态形状感知的端到端优化，使大语言模型在多种GPU上达到先进性能并支持更广泛设备部署。
2025-02-07 cs.AI cs.LG cs.PL
