paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Syntax and Semantics for Operations with Scopes

带作用域操作的语法与语义
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文属于纯 PL 形式语义与范畴论研究,讨论代数效应/处理器的语法与语义分离,并未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。仅在广义 PL 理论基础上有轻微关联,与用户当前研究画像匹配度较低。引用 26 inbox
Maciej Piróg, Tom Schrijvers, Nicolas Wu, Mauro Jaskelioff
crossref: 2026-09-12

AI 速览

一句话:提出带作用域操作的抽象语法的范畴模型,以分离代数效应与处理器的语法和语义。

本文针对代数效应与 handlers 编程中语法与语义难以分离的问题,提出一种带作用域操作(scoped operations)的抽象语法的范畴模型。与普通树节点不同,带作用域操作能够包含项的一整部分,即作用域;异常处理中的 catch 和非确定性计算中的 once 是典型例子。论文强调这类操作在程序组合即语法替换下的行为,并借助范畴结构给出语法与语义的抽象刻画。该工作为统一描述作用域操作的语法、替换与语义提供了理论基础,并通过实例说明模型能覆盖常见的效应操作。全文为理论建模,未报告实验评估。

问题
在代数效应与 handlers 中,如何将语法与语义分离,并统一处理那些会包围一部分项的带作用域操作。
方法
提出带作用域操作的抽象语法的范畴模型,将作用域操作视为可包含项的一部分的构造,并刻画其在语法替换下的行为。
评估
通过 catch(异常处理)和 once(非确定性选择)等程序例子说明模型适用性;属于理论工作,无实验评估。
原文摘要(Abstract)

Motivated by the problem of separating syntax from semantics in programming with algebraic effects and handlers, we propose a categorical model of abstract syntax with so-called scoped operations. As a building block of a term, a scoped operation is not merely a node in a tree, as it can also encompass a whole part of the term (a scope). Some examples from the area of programming are given by the operation catch for handling exceptions, in which the part in the scope is the code that may raise an exception, or the operation once, which selects a single solution from a nondeterministic computation. A distinctive feature of such operations is their behaviour under program composition, that is, syntactic substitution.

链接与引用

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

BibTeX
@inproceedings{paperbot4367,
  title = {Syntax and Semantics for Operations with Scopes},
  author = {Maciej Piróg and Tom Schrijvers and Nicolas Wu and Mauro Jaskelioff},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209166}
}