paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Flix: A Design for Language-Integrated Datalog

Flix:一种语言集成 Datalog 的设计
OOPSLA 9(OOPSLA2)2025匹配度 5/10 · 论文提出 Flix 的语言集成 Datalog,支持模块化、多态和类型化的 Datalog 程序,并以 IFDS/IDE 等程序分析算法为例,属于静态分析与程序语言基础设施,与用户对程序分析的兴趣有交集;但未涉及 LLM/Agentic 程序、浮点程序分析或贝叶斯程序分析,因此不是核心方向。引用 0 inbox
Magnus Madsen, Ondřej Lhoták
crossref: 2026-09-10

AI 速览

一句话:提出 Flix 中语言集成 Datalog 的设计,使 Datalog 程序可模块化、多态、类型化地复用于程序分析等任务。

论文综述 Flix 编程语言中的 Datalog 设施。问题在于如何在通用语言中以模块化、可复用且类型安全的方式编写和组合 Datalog 程序。方法上,Flix 将 Datalog 程序作为一等值,引入 rho 抽象、参数多态和类型类,并提供 inject/query 程序构造、head/guard 表达式、函数式谓词和格语义等特性,从而增强表达力与易用性。评估上,作者用 Ullman 分层算法、Ford-Fulkerson 最大流以及上下文敏感程序分析中的 IFDS 和 IDE 算法等应用进行说明,并给出这些算法的完全模块化、多态、类型化与声明式实现,可实例化到任意抽象域。

问题
如何让通用编程语言以语言集成的方式支持 Datalog 程序,并使其具备模块化、可复用、多态与类型安全等特性。
方法
Flix 将 Datalog 程序提升为一等值,借助 rho 抽象、参数多态、类型类以及 inject/query、head/guard、函数式谓词、格语义等构造来集成 Datalog。
评估
通过 Ullman 分层、Ford-Fulkerson 最大流、IFDS/IDE 等应用展示设计,并实现可实例化任意抽象域的模块化、多态、类型化声明式分析算法。
原文摘要(Abstract)

We present a comprehensive overview of the Datalog facilities in the Flix programming language. We show how programmers can write functions implemented as Datalog programs and we demonstrate how to build modular and reusable families of Datalog programs using first-class Datalog program values, rho abstraction, parametric polymorphism, and type classes. We describe several features that improve the ergonomics, flexibility, and expressive power of Datalog programming in Flix, including the inject and query program constructs, head and guard expressions, functional predicates, lattice semantics, and more. We illustrate Datalog programming in Flix with several applications, including implementations of Ullman's algorithm to stratify Datalog programs, the Ford-Fulkerson algorithm for maximum flow, and the IFDS and IDE algorithms for context-sensitive program analysis. The implementations of IFDS and IDE fulfill a long-term goal: to have fully modular, polymorphic, typed, and declarative formulations of these algorithms that can be instantiated with any abstract domain.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3009,
  title = {Flix: A Design for Language-Integrated Datalog},
  author = {Magnus Madsen and Ondřej Lhoták},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763126}
}