paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A monad for full ground reference cells

面向完全基类型引用单元的 monad
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 该论文属于程序语言形式语义与指称语义,讨论可含环引用单元的 monad 与效应屏蔽,虽与形式化验证/代码变换有间接关联,但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等画像核心方向。引用 22 inbox
Ohad Kammar, Paul B. Levy, Sean K. Moss, Sam Staton
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:用函子范畴上的 monad 给出可含环引用单元的指称语义,并支持效应屏蔽与代码变换验证。

本文研究动态分配、且可能形成环形结构的引用单元的指称语义问题,特别关注局部状态封装(效应屏蔽)的语义刻画。作者将堆(heaps)视为某个函子范畴中的对象,并在其上构造一个用于为堆添加隐藏/封装能力的 monad;随后通过将状态 monad 变换器作用于该封装 monad,得到支持效应屏蔽的完全基类型引用(full ground references)的 monad。为评估该 monad,作者为一个带完全基类型引用的 call-by-value 演算给出了指称语义,并据此验证了相关的代码变换(等式推理)。该工作为含共享与环的内存单元提供了一种范畴论式的统一语义框架。

问题
如何为动态分配、可能含环的引用单元给出指称语义,并刻画局部状态的封装/效应屏蔽?
方法
在函子范畴上构造堆对象与封装 monad,并用状态 monad 变换器组合出支持效应屏蔽的完全基类型引用 monad。
评估
为一个带完全基类型引用的 call-by-value 演算给出指称语义,并验证相应的代码变换(等式法则)。
原文摘要(Abstract)

We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

链接与引用

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

BibTeX
@inproceedings{KammarLMS17,
  title = {A monad for full ground reference cells},
  author = {Ohad Kammar and Paul B. Levy and Sean K. Moss and Sam Staton},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005109}
}