$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
本文提出 ωPAP 空间范畴作为指称语义框架，以统一处理高阶递归概率与可微程序，并据此证明自动微分正确性及概率程序迹密度的几乎处处可微性。
2023-05-25 cs.LG cs.LO cs.PL
Towards univalent reference types
本文在 guarded homotopy type theory 中为一般引用类型发展了指称语义，首次揭示了 univalence 对可变状态语义的深远影响，自动确保计算在堆对称性下不变，从而提供丰富的程序等价性。
2023-11-21 cs.LO
Denotational Foundations for Expected Cost Analysis
本文提出基于按值传递调用（CBPV）的元语言 cert，定义代价与期望代价两种指称语义，证明其可靠性、充分性及效应模拟性质，并通过案例展示其表达能力。
2025-02-26 cs.LO cs.PL
Universal Semantics for the Stochastic Lambda-Calculus
我们为随机λ演算定义了合理的和充分的指称和操作语义。这两种语义方法建立在以前的工作，使用类似的技术来推理高阶概率程序，但第一次承认一个充分性定理有关的操作和指称的意见。这解决了（Bacci等人，2018）中未解决的主要问题。
2021-05-14 cs.LO
Upper approximating probabilities of convergence in probabilistic coherence spaces
我们开发了一个理论的概率相干空间配备了一个额外的扩展结构，并将其应用于近似概率PCF的自由变量是地面类型的地面类型程序的收敛概率。为此，我们定义了一个适应版本的Krivine机计算多项式近似的这些程序的语义模型。这些多项式提供近似从下面和从上面的收敛概率;这是可能的，通过扩展语言的错误符号，这是扩展最大的模型。
2020-08-11 cs.LO cs.PL
Probabilistic Rely-guarantee Calculus
Jones的可靠保证演算共享变量并发扩展到包括概率行为。我们使用的代数方法，结合和适应概率Kleene代数并发Kleene代数。稳健的代数相对于一般的概率事件结构语义。本文的主要贡献是建立在语义之上的可靠保证规则的集合。特别是，我们展示了如何获得的概率范围内的真实并发指称语义的可靠保证规则。这些规则的使用说明了一个简单的概率并发程序的详细验证：一个错误的Eratosthenes筛。
2015-06-02 cs.LO
Towards a Higher-Order Bialgebraic Denotational Semantics
University of Birmingham（伯明翰大学）；University of Southern Denmark（南丹麦大学）；Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
本文发展了高阶抽象GSOS中的适当指称语义理论，通过局部终余代数构造语义域，解耦于语法，适用于多种高阶语言。
2026-07-01 cs.LO cs.PL
Evidence-Tracked Tape Semantics for Probabilistic Computation
Ben-Gurion University（本-古里安大学）
本文提出证据追踪带语义，通过monadic-core-to-evidenced-frame流程，建立高阶逻辑，使概率计算的证据转换和量化陈述得以体现。
2026-05-08 cs.LO
A polytime complexity analyser for Probabilistic Polynomial Time over imperative stack programs
我们提出了iSAPP（概率多项式时间的强制静态分析器），一个复杂性验证工具，是健全的和扩展完整的概率多项式时间（PP）的复杂性类。iSAPP工作在用于堆栈机器的命令式程序设计语言上。多项式的证书可以根据所使用的堆栈的数量在多时间中构建。
2013-04-11 cs.CC cs.LO
Deterministic stream-sampling for probabilistic programming: semantics and verification
本文提出以采样器为核心的高阶概率编程语言及其连续映射语义，并通过类型系统处理不连续操作，进而给出采样器等价推理与正确性证明的形式化演算。
2023-04-26 cs.LO cs.PL
Semantics for Variational Quantum Programming
我们考虑一个程序设计语言，可以操纵经典和量子信息。我们的语言是类型安全的，设计用于变分量子编程，这是一个混合的经典量子计算范式。该语言的经典子系统是概率定点演算（PFPC），它是一个具有混合方差递归类型、项递归和概率选择的λ演算。量子子系统是一个可以操纵量子信息的一阶线性系统。这两个子系统通过混合的经典/量子项相关联，这些项指定了经典概率效应如何由量子测量引起，以及相反地，经典（概率）程序如何影响量子动力学。我们还描述了一个声音和计算足够的指称语义的语言。经典的概率效应解释使用最近描述的交换概率单子DCPO。量子效应和资源被解释在一类冯诺依曼代数，我们显示是丰富的（连续）域。这种强烈的丰富感使我们能够开发新的语义方法，我们用来解释量子和经典概率效应之间的关系。通过这样做，我们提供了第一个指称的分析，涉及模型的经典概率规划模型的量子规划。
2021-07-28 cs.LO cs.PL math.CT
Generating Functions for Probabilistic Programs
本文研究了离散概率规划推理中生成函数（GF）在程序变量上的编码度量的使用。为此，我们定义了一个指称的GF-Transformer语义的概率while程序，并表明它实例化Kozen的种子分布Transformer语义。然后我们研究了GF在程序分析中的有效使用。我们表明，可表达的GF使检查超不变量的计算机代数工具，它们可以用来确定终止概率。最后，本文描述了一类-可能是无限状态-程序的语义是一个合理的GF编码离散相位型分布。
2020-07-13 cs.LO cs.PL
Denotational semantics for languages for inference: semirings, monads, and tensors
本文通过半环视角研究推理语言的代数理论，探讨单子、半环与张量的联系，并证明在若干概率例子中半环张量能决定子理论的张量。
2023-12-27 cs.LO cs.PL math.CT
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
Formal Semantics of a Classical-Quantum Language
我们调查的形式语义的一个简单的命令式语言，具有经典和量子结构。更具体地说，我们提供了一个操作语义，一个指称语义和两个霍尔风格的证明系统：一个抽象的和一个具体的。这两个证明系统是基于满意度的，灵感来自于Barthe等人的概率程序的程序逻辑。抽象的证明体系是健全的、相对完整的，而具体的证明体系只是健全的。
2021-07-02 cs.LO
Measurable Cones and Stable, Measurable Functions
定义了锥间稳定可测映射的概念，并给出了可测性检验，证明了它构成了一个cpo-丰富的carnival闭范畴。这一类给出了一个指称模型的PCF支持概率函数编程的主要原语，如连续和离散概率分布，采样，条件和全递归的扩展。我们证明了这个模型的合理性和充分性，就按名称调用的操作语义，并给出了一些例子，它的外延。
2017-11-27 cs.LO cs.PL
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
本文提出基于概率生成函数语义的精确贝叶斯推断方法，并实现 Prodigy 工具，以支持含无界循环的条件化概率程序的推断与定量验证。
2024-03-05 cs.LO cs.PL
Probabilistic modal μ-calculus with independent product
概率模态μ-演算是一种不动点逻辑，用于表示概率标记变迁系统（PLTS）的性质。两个等价的语义已经研究了这个逻辑，都分配给每个状态一个值在区间[0，1]表示的概率，该公式表示的属性在状态保持。一种语义是指称的，另一种是游戏语义，指定在两个玩家的随机奇偶游戏。概率模态μ演算的一个缺点是缺乏对PLTS的其他重要时态逻辑（如概率计算树逻辑（PCTL））进行编码所需的表达能力。为了解决这个问题，我们扩展了一对新的运营商的逻辑：独立产品和余产品。由此产生的逻辑，称为概率模态μ演算与独立的产品，可以编码许多感兴趣的属性，并纳入定性片段的PCTL。本文的主要贡献是为这种扩展的概率μ演算定义了一个合适的博弈语义。这依赖于一类新的游戏的定义，它通过允许一个游戏被分成并发的子游戏，每个子游戏独立地继续它们的进化，来概括标准的两个玩家随机（奇偶）游戏。我们的主要技术结果是两个语义的等价性。证明是在ZFC集合论中进行的，在不可数基数上扩展了Martin公理。
2012-11-26 cs.LO
Convexity and Order in Probabilistic Call-by-Name FPC
本文从范畴论视角证明Kegelspitzen结构可建模随机矩阵至域范畴，构成概率编程语言pPCF的指称模型，并讨论递归类型的解释。
2020-11-11 cs.LO cs.PL
Commutative Monads for Probabilistic Programming Languages
在支持概率选择的程序设计语言的语义中，一个长期存在的公开问题是在DCPO范畴上找到概率的交换单子。在本文中，我们提出了三个这样的单子和一个一般的建设，以寻找更多。我们将展示如何使用这些单子提供一个健全的和足够的指称语义的概率定点演算（PFPC）-调用值简单类型的λ演算与混合方差递归类型，长期递归和概率选择。我们还表明，在特殊的情况下，我们认为连续dcpo的，那么所有三个单子符合估值单子的琼斯和我们充分的诱导Eilenberg-Moore类别表明，他们都同构的范畴连续Kegelspitzen的凯梅尔和Plotkin。
2021-01-31 cs.LO cs.PL math.CT
Compositional Semantics for Probabilistic Programs with Exact Conditioning
University of Oxford（牛津大学）
我们定义了一个概率程序设计语言的高斯随机变量与一流的精确条件构造。我们给这种语言的操作，指称和等式语义，建立方便的属性，如交换条件。连续随机变量相等的条件是非平凡的，因为精确的观察可能有概率为零;这是波莱尔悖论。使用条件概率的分类公式，我们表明，我们的语言的良好性能是不特定的高斯，但可以从普遍的属性，从而推广到更广泛的设置。我们定义的Cond建设，它内在的条件作为一个态射，提供一般的组合语义的概率编程与精确的条件。
2021-01-27 cs.AI cs.LO cs.PL
An Adequate While-Language for Stochastic Hybrid Computation
本文提出一种可形式化推理随机混合计算程序的 While 语言，涵盖微分与概率构造，并给出操作语义、解释器、指称语义及两者间的充分性定理。
2025-07-21 cs.LO
Discrete time stochastic and deterministic Petri box calculus
我们提出了一个扩展的确定性定时多作用的离散时间随机和立即Petri盒演算（dtsiPBC），以前提出的I.V.Tarasyuk，H。Macià和V. Valero。在dtsdPBC中，非负整数指定具有固定（包括零）时间延迟的多操作。步骤操作语义是通过标记的概率转移系统构造的。基于带确定性变迁的带标签离散时间随机Petri网的一个子类定义了其指称语义。这两种语义的一致性证明。为了评估性能，相应的半马尔可夫链和（减少）离散时间马尔可夫链进行了分析。
2019-05-01 cs.LO
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
本文在守护类型论中利用高阶归纳类型和守护递归建模带概率选择与递归类型的语言，并建立操作与指称语义间的关系以支持充分性和上下文等价推理。
2024-10-24 cs.LO cs.PL
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
我们研究互模拟和上下文等价的概率$λ$演算。本文的贡献有三个方面。首先，我们展示了一种证明概率应用双相似同余的技术。虽然该技术遵循豪的方法，但一些技术细节是完全不同的，依赖于实数集的非平凡“解开”属性。其次，我们表明，虽然双相似性是在一般情况下严格比上下文等价，这两个关系之间的重合达到纯$λ$ -条款。由此产生的等式是由Levy-Longo树诱导的等式，通常被认为是在懒惰制度下纯$λ$ -项上的最好的扩展等价。最后，我们推导出一个共归纳特征的上下文等价的整个概率语言，通过一个扩展，其中条款类似于分布可能会出现在redex的位置。扩展的另一个动机是它的操作语义允许我们实验不同的一致性技术，即逻辑双相似性。
2013-11-07 cs.LO cs.PL
A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems
Yale University（耶鲁大学）；SingularityNET（奇点网）
我们引入了一个正式的元语言的概率编程，能够表达程序和类型系统中，他们被嵌入。我们的动机是希望AGI不仅学习相关知识（程序/证明），而且学习适当的推理方式（逻辑/类型系统）。我们利用立方类型论和依赖类型元图的框架来形式化我们的方法。在这样做时，我们表明，元语言中的特定结构可以通过互模拟（意味着路径等价）与它们对应的类型系统相关。这使得我们的方法提供了一种方便的方法来派生合成指称语义的各种类型系统。特别是，我们推导出纯型系统（PTS）和概率依赖型系统（PDTS）的互模拟。我们进一步讨论了PTS的关系，非良基集理论，并证明了我们的方法的可行性与实现的互模拟证明在一个守护立方类型论类型检查。
2022-08-16 cs.AI cs.FL 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
Probability and Angelic Nondeterminism with Multiset Semantics
针对幂集与Giry单子间缺乏分配律的问题，提出带天使型非确定性的概率克林代数及自动机类，用多重集分布实现语义，得出克林定理、余代数理论等关键结果，解决理论障碍。
2025-04-17 cs.FL cs.LO cs.PL
Smart Choices and the Selection Monad
Google Research（谷歌研究院）
从编程语言视角定义两种支持决策抽象的小型语言，基于选择单子给出操作与指称语义，证明两者一致并建立基础类型上的完全抽象与完备性。
2023-04-19 cs.LG cs.LO cs.PL
Bayesian Separation Logic
贝叶斯分离逻辑（BaSL）通过概率分离逻辑框架，实现了对贝叶斯概率编程语言核心概念如贝叶斯更新、非归一化分布等的建模，同时保持语义的模块性和兼容性。
2025-12-01 cs.LO cs.PL
Backpropagation for Effectful Languages I: Finite Probability and Discrete Output Algebraic Effects
Utrecht University（乌得勒支大学）；Centre for Mathematics, University of Coimbra（科英布拉大学数学中心）
研究离散概率程序的反向模式自动微分，基于CHAD框架，以有限原子分布单子为例，定义反向模式代码变换并证明其正确性，为离散输出代数效应微分提供可复用模式，是扩展CHAD的基础步骤。
2026-07-29 cs.LO cs.PL math.CT
Incremental Computation for Efficient Programmable Inference in Probabilistic Programs
Massachusetts Institute of Technology（麻省理工学院）；Yale University（耶鲁大学）
提出基于增量计算的方法，将概率程序编译为确定性密度函数，并通过增量λ演算实现函数式程序的增量计算，以加速蒙特卡洛推理，支持非参数模型，并保证正确性。
2026-06-03 cs.LO cs.PL stat.CO
Abstract Hidden Markov Models: a monadic account of quantitative information flow
本文提出抽象隐马尔可夫模型作为概率隐藏状态程序的指称语义，利用Giry单子编码隐藏状态，推广熵度量并建立向后不确定性变换子，揭示Dalenius要求本质是组合性问题。
2019-03-28 cs.LO
Quantum Orchestras: a Concrete Semantics for Recursive Hybrid Programs
The University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）
研究为扩展经典基础语言的量子编程语言构建指称语义的方法，通过定义基于量子仪器形式主义的量子管弦乐队单子，它是经典状态单子和概率幂域单子的自然扩展，可解释发散混合程序并研究扩展到量子非交换情况的微妙之处。
2026-07-13 cs.LO cs.PL quant-ph
