Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are ``separate'', i.e., when programs do not interfere with each other, it can be easier to reason about them. While reasoning about separated resources has been well-studied, there has been little work on reasoning about separated effects, especially for functional, higher-order programming languages. We propose two higher-order languages that can reason about sharing and separation in effectful programs. Our first language $\lambda_{\text{INI}}$ has a linear type system and probabilistic semantics, where the two product types capture independent and possibly-dependent pairs. Our second language $\lambda_{\text{INI}}^2$ is two-level, stratified language, inspired by Benton's linear-non-linear (LNL) calculus. We motivate this language with a probabilistic model, but we also provide a general categorical semantics and exhibit a range of concrete models beyond probabilistic programming. We prove soundness theorems for all of our languages; our general soundness theorem for our categorical models of $\lambda_{\text{INI}}^2$ uses a categorical gluing construction.

翻译：效应性程序之间的交互超越了简单的输入输出关系，这使得组合推理变得具有挑战性。已有研究表明，当此类程序相互“分离”（即程序彼此不干扰）时，对其推理更容易。尽管针对分离资源的推理已得到充分研究，但针对分离效应的推理（尤其是在函数式高阶编程语言中）的工作尚属少见。我们提出了两种能够对效应性程序中的共享与分离进行推理的高阶语言。第一种语言 λ_INI 采用线性类型系统和概率语义，其中两种乘积类型分别捕获独立对与可能相关对。第二种语言 λ_INI^2 是受 Benton 的线性-非线性（LNL）演算启发的双层分层语言。我们以概率模型为例对该语言进行阐释，同时提供了通用的范畴语义，并展示了除概率编程之外的一系列具体模型。我们为所有语言证明了可靠性定理；其中针对 λ_INI^2 范畴模型的通用可靠性定理采用了范畴胶合构造方法。