Probabilistic Stable Functions on Discrete Cones are Power Series (long version)
本文研究了可测锥和可测稳定函数范畴Cstabm，它是一个具有连续概率和全递归的高阶语言的指称模型。我们把Cstabm看作是离散概率的模型，通过展示一个carnival封闭的、完整的和忠实的函子的存在，该函子将概率相干空间（一个完全抽象的具有完整递归和离散概率的高阶语言的指称模型）嵌入Cstabm。证明是基于一个推广的伯恩斯坦定理从真正的分析允许看到稳定的功能之间的离散锥广义幂级数。
2018-05-01 cs.LO
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
The University of Tokyo（东京大学）；University of Bologna（博洛尼亚大学）；Aix Marseille Univ, Université de Toulon, CNRS, LIS（艾克斯-马赛大学，土伦大学，法国国家科学研究中心，信息系统实验室）
本文针对概率高阶模型检查问题展开研究，引入PHORS作为概率高阶程序模型，证明二阶PHORS几乎必然终止性不可判定，给出终止概率不动点刻画并实现了近似计算过程，经初步实验验证其运行良好。
2026-08-20 cs.LO cs.PL
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
本文提出一个范畴框架，通过denotational积构造将效应高阶程序的线性时间安全性验证归约为最弱前置条件计算，并实现了首个支持递归概率高阶程序的自动化验证器。
2025-10-17 cs.LO
A coalgebraic higher-order modal fixed-point logic
University of Sheffield（谢菲尔德大学）
研究引入高阶模态不动点逻辑的余代数扩展，包含HFL及其概率扩展，证明非确定性有限自动机空集问题和概率自动机值为1问题可归结为该余代数形式的模型检查问题。
2026-07-22 cs.LO
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
本文提出Clutch，一种支持异步概率耦合的高阶概率关系分离逻辑，用于推理高阶程序的上下文精化与等价性，并在Coq中形式化验证。
2023-11-14 cs.LO cs.PL
Semantics of higher-order probabilistic programs with conditioning
University College London（伦敦大学学院）；Cornell University（康奈尔大学）
我们提出了一个指称语义高阶概率规划的线性算子之间的Banach空间。我们的语义是植根于经典理论的Banach空间及其张量积，但承担的相似之处与著名的斯科特语义的高阶程序通过使用有序的Banach空间，允许定义的不动点。基于一个monoidal而不是carnival封闭结构，我们的语义有效地把随机性作为一种资源。
2019-02-28 cs.LG cs.LO cs.PL
On Probabilistic Applicative Bisimulation and Call-by-Value $λ$-Calculi (Long Version)
概率应用互模拟是一个最近推出的共归纳方法程序等价的概率，高阶，设置。在本文中，该技术被应用到一个类型化的，按值调用，演算。令人惊讶的是，所获得的关系符合上下文等价，相反，当调用的名字被认为是评估时会发生什么。更令人惊讶的是，完全抽象只适用于对称设置。
2014-01-29 cs.LO
Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals
概率团队语义是概率依赖的逻辑分析框架。我们的重点是概率包含逻辑及其扩展的公理化，复杂性和表达性。我们确定了一个自然片段的存在性二阶逻辑与添加剂真正的算术，准确地捕捉概率包含逻辑的表达能力。此外，我们将这些形式主义的线性规划，这样做得到PTIME数据复杂度的逻辑。此外，在有限结构上，我们证明了具有加性实算术的完全存在二阶逻辑只能表示NP性质。最后，我们在原子层次上给出了概率包含逻辑的一个合理而完整的公理化。
2021-12-21 cs.LO
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
我们研究互模拟和上下文等价的概率$λ$演算。本文的贡献有三个方面。首先，我们展示了一种证明概率应用双相似同余的技术。虽然该技术遵循豪的方法，但一些技术细节是完全不同的，依赖于实数集的非平凡“解开”属性。其次，我们表明，虽然双相似性是在一般情况下严格比上下文等价，这两个关系之间的重合达到纯$λ$ -条款。由此产生的等式是由Levy-Longo树诱导的等式，通常被认为是在懒惰制度下纯$λ$ -项上的最好的扩展等价。最后，我们推导出一个共归纳特征的上下文等价的整个概率语言，通过一个扩展，其中条款类似于分布可能会出现在redex的位置。扩展的另一个动机是它的操作语义允许我们实验不同的一致性技术，即逻辑双相似性。
2013-11-07 cs.LO cs.PL
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Aarhus University（奥胡斯大学）；New York University（纽约大学）；Amazon Web Services（亚马逊云科技）
本文提出Foxtrot，首个用于证明高阶并发概率程序上下文细化的高阶分离逻辑，结合了并发推理原理与概率推理原理，展示了其在对抗性von Neumann硬币和Sodium加密库中的应用。
2026-04-27 cs.LO cs.PL
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
University of Bath（巴斯大学）
本文提出利用热带几何工具对高阶概率程序进行统计推断，通过关联程序与度数和多面体，设计交类型系统以高效估计最可能运行。
2025-11-20 cs.LO
$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
本文提出 ωPAP 空间范畴作为指称语义框架，以统一处理高阶递归概率与可微程序，并据此证明自动微分正确性及概率程序迹密度的几乎处处可微性。
2023-05-25 cs.LG cs.LO cs.PL
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
我们介绍了高阶量子计算的相互作用几何模型，并证明了它的充分性的一个完整的量子程序设计语言，其中纠缠，复制和递归都是可用的。我们的模型带有多令牌机，证明网系统和PCF风格的语言。我们开发的方法并不特定于量子计算，我们的模型是一个新框架的实例，其主要特征是能够在并行环境中模拟交换效应。它基于一个多令牌机，配备了内存，它具有具体的性质，这使得它非常适合于建立低层次的高阶语言的操作描述。
2017-07-15 cs.LO
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
对抗性计算是一类被广泛研究的计算，其中资源受限的概率对手可以访问预言机，即，概率过程与私人状态这些计算经常出现在几个领域，包括安全，隐私和机器学习。在本文中，我们开发了程序逻辑，用于在高阶设置中推理对抗计算。我们的逻辑是建立在一个简单类型的$λ$ -演算扩展与分级单子的概率和状态。分级用于建模和限制计算的内存占用和成本（就Oracle调用而言）。在这种观点下，对手是一个高阶表达式，它期望其神谕的代码作为参数。我们开发了一元程序逻辑推理的错误概率和期望值，和一个关系逻辑推理的耦合为基础的属性。所有逻辑都具有对抗计算的规则，并且对满足固定资源策略的所有对手都有效的产量保证。我们证明了健全的逻辑在类的准Borel空间，使用一个一般概念的分级谓词提升，我们使用逻辑关系分级谓词提升建立健全的证据规则的对手。我们用简单但说明性的例子来说明我们的逻辑的工作。
2021-07-02 cs.LO cs.PL
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
2025-08-07 cs.LO cs.PL
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
本文提出高阶近似关系分离逻辑 Approxis，通过误差信用支持概率高阶有状态程序的近似与精确等价推理，并在 Coq/Iris 中机械化验证安全与采样示例。
2024-12-03 cs.LO cs.PL
Step-Indexed Logical Relations for Probability (long version)
众所周知，构造高阶概率程序设计语言的模型是具有挑战性的。我们将展示如何构建一个高阶程序设计语言的概率扩展的步骤索引的逻辑关系，不谓词多态性和递归类型。我们表明，由此产生的逻辑关系是健全的和完整的上下文前序，而且，它是方便的推理具体的程序等价。最后，我们扩展的语言与动态分配的一阶引用，并显示如何扩展的逻辑关系，这种语言。我们表明，由此产生的关系仍然是有用的推理涉及国家和概率选择的例子。
2015-01-13 cs.LO
An Expressive Probabilistic Temporal Logic
本文认为，概率，时间和行动的综合治疗是必不可少的概率的概念的适当的逻辑帐户，并根据这种直觉，描述了一个表达概率的时间逻辑推理的行动与不确定的结果。该逻辑是模态的和高阶的：由动作注释的模态用于表达由动作产生的下一状态中的命题的可能性和必要性，并且需要高阶函数来表达概率算子。所提出的逻辑被证明是经典数学概率论的一个适当的扩展，并通过Monty Hall问题的形式化来说明其表达能力。
2017-10-08 cs.AI cs.LO
A Domain Theory for Statistical Probabilistic Programming
我们给出了一个足够的指称语义的语言递归高阶类型，连续概率分布，和软约束。这些是用于构建计算统计和机器学习中使用的贝叶斯模型的表达语言。其中包括无类型语言，类似于Church和WebPPL，因为我们的语义允许递归混合方差数据库。我们的语义证明了重要的程序等价性，包括交换性。我们的新语义模型是基于“准Borel predomains”。它们是链完全偏序（cpos）和拟波莱尔空间的混合。拟波莱尔空间是概率论的一个新模型，它主要研究可容许随机元的集合。在cpo模型中，传统上使用概率幂域来处理概率，但不知道这些幂域在任何具有高阶函数的cpo上都是可交换的。相比之下，拟Borel前域支持交换概率幂域和高阶函数。正如我们所示，准Borel predomains形式的菲奥雷的公理域理论和模型的科克的综合措施理论。
2021-07-29 cs.LO cs.PL
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
针对现有方法无法为高阶概率程序提供精确误差界的问题，本文提出含“错误信用”资源的高阶分离逻辑Eris，支持新推理原则，能证明哈希碰撞等场景的摊销误差界及拒绝采样算法的正确性，且结果已机械化验证。
2024-11-29 cs.LO cs.PL
Probabilistic Obstruction Temporal Logic: a Probabilistic Logic to Reason about Dynamic Models
该研究提出新型概率逻辑POTL，扩展阻碍逻辑并加入概率元素，可用于攻防策略交互推理，且模型检测复杂度不高于PCTL，适用于网络安全隐私领域。
2024-10-28 cs.GT cs.LO
A Higher-Order Language for Markov Kernels and Linear Operators
为概率程序设计语言赋予语义已经做了很多工作。近年来，大多数用于概率程序推理的语义分为两类：基于马尔可夫核的语义和基于线性算子的语义。这两种风格的语义都在概率程序的推理中找到了许多应用，但它们都有自己的优点和缺点。虽然人们认为它们之间有联系，但没有语言可以处理这两种风格的编程。在这项工作中，我们解决这些问题，通过定义一个两级演算和它的分类语义，这使得有可能与这两种语义的程序。从逻辑的角度来看，我们将这种语言视为线性逻辑的替代资源解释，其中跟踪的资源是采样而不是变量使用。
2023-03-02 cs.LO cs.PL
Separated and Shared Effects in Higher-Order Languages
高效的程序交互方式超越了简单的输入输出，这使得组合推理具有挑战性。现有的工作表明，当这些程序是“分离的”时，即，当程序之间互不干扰时，对它们的推理就更容易了。虽然关于分离资源的推理已经得到了很好的研究，但是关于分离效果的推理的工作很少，特别是对于函数式的高阶程序设计语言。我们提出了两种高阶语言，可以在有效的程序中进行共享和分离。我们的第一种语言$λ_{\text{INI}}$具有线性类型系统和概率语义，其中两种产品类型捕获独立和可能依赖的对。我们的第二语言$λ_{\text{INI}}^2$是两级的，分层的语言，灵感来自本顿的线性非线性（LNL）演算。我们激励这种语言的概率模型，但我们也提供了一个一般的分类语义，并表现出一系列的具体模型超出概率编程。我们证明我们所有的语言的合理性定理，我们的一般合理性定理，我们的分类模型$λ_{\text{INI}}^2$使用分类胶合建设。
2023-03-02 cs.LO cs.PL
Probabilistic Termination by Monadic Affine Sized Typing (Long Version)
我们引入了一个系统的一元仿射大小的类型，这基本上概括了通常的大小类型，并允许这种方式来捕捉概率高阶程序几乎肯定终止。超越普通的、强规范化而不失去可靠性是一项艰巨的任务，如果没有更丰富的、定量的类型概念，而且没有施加一些亲和性约束，这是无法完成的。建议的类型系统是强大的，足以类型的经典例子的概率终止程序，如随机游走。类型化程序被证明几乎必然终止的方法是基于归约的，但需要对该技术进行实质性的修改。
2017-01-15 cs.LO cs.PL
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
本文提出高阶分离逻辑Tachis，通过引入概率成本信用资源来推理概率程序的期望成本，支持摊还分析与多种成本模型，并经Coq等工具机械化验证了多种算法的期望成本上限。
2024-11-12 cs.LO cs.PL
Convexity and Order in Probabilistic Call-by-Name FPC
本文从范畴论视角证明Kegelspitzen结构可建模随机矩阵至域范畴，构成概率编程语言pPCF的指称模型，并讨论递归类型的解释。
2020-11-11 cs.LO cs.PL
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO cs.PL
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
Aarhus University（奥胡斯大学）；New York University（纽约大学）；Amazon Web Services（亚马逊云科技）
本文提出一种适用于复杂通用编程语言中差分隐私实现验证的程序逻辑，支持隐私预算作为分离逻辑资源的推理，可处理隐私过滤器和缓存等常见编程模式，并通过实现验证的差分隐私库展示其通用性和可重用性。
2026-04-14 cs.LO cs.PL
First-Order Context-Specific Likelihood Weighting in Hybrid Probabilistic Logic Programs
KU Leuven（荷语鲁汶大学）；Czech Technical University in Prague（布拉格捷克理工大学）
到目前为止，统计关系AI和概率逻辑编程主要集中在离散概率模型上。这样做的原因是，需要提供结构来简洁地建模这种模型中的独立性，并提供有效的推理。三种类型的独立性是很重要的表示和利用混合模型中的可扩展推理：条件独立性优雅地建模在贝叶斯网络中，上下文特定的独立性自然表示的逻辑规则，和独立性之间的相关对象的属性在关系模型简洁地表示组合规则。本文介绍了一种结合贝叶斯逻辑程序中分布子句的语法和语义原理的混合概率逻辑程序设计语言DC #。它定性地代表了三种独立性。更重要的是，我们还介绍了DC #的可扩展推理算法FO-CS-LW。FO-CS-LW是上下文特定似然加权算法（CS-LW）的一阶扩展，CS-LW是一种利用地面模型中的条件独立性和上下文特定独立性的新型采样方法。FO-CS-LW算法将具有统一和组合规则的CS-LW算法提升到一阶情况。
2023-01-08 cs.AI cs.LO
Metric Structures and Probabilistic Computation
连续一阶逻辑用于将模型理论分析应用于分析结构（例如希尔伯特空间、巴拿赫空间、概率空间等）。经典可计算模型论用于研究可以用经典一阶逻辑描述的数学对象的算法结构。本文表明，概率计算（有时称为随机计算）可以发挥类似的作用，在连续一阶逻辑中描述的结构。本文的主要结果是一个有效的完备性定理，证明了每一个可判定的连续一阶理论都有一个概率可判定的模型。后面的章节给出了这个框架应用于各类结构和计算复杂性理论的一些问题的例子。
2008-06-02 cs.LO math.FA math.LO
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
