一句话：提出范畴论逻辑关系构造，为带和类型、效应操作与基元的计算 λ-演算生成可靠且完全抽象的模型。
论文研究如何为含效应、和类型与基元的 λ-演算构造既可靠又完全抽象的语义模型。作者在适当假设下，从 Moggi 计算 λ-演算的模型出发，借助纤维化、范畴 glueing、⊤⊤-lifting 与 ⊤⊤-closure 等技术，构造出一个新的模型，其思路受 O'Hearn 与 Riecke 的 PCF 完全抽象模型启发。关键结果是该模型满足 adequacy 与 full abstraction，并可在集合与函数范畴、微分空间与光滑映射范畴以及 quasi-Borel 空间范畴中应用；后者已被用于可微编程与概率编程的语义研究。
We present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lifting, and ⊤⊤-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming.
@article{paperbot1555,
title = {Fully abstract models for effectful λ-calculi via category-theoretic logical relations},
author = {Ohad Kammar and Shin-ya Katsumata and Philip Saville},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498705}
}