介绍了赋予高阶函数和连续分布的概率编程语言的新概率论形式化 —— 拟 Borel 空间。展示了拟 Borel 空间可以替代标准可测空间、支持高阶函数、支持等式推理证明、同时支持连续概率分布，并将其运用于高阶函数与概率的理论证明。

Jan, 2017

本文研究表达丰富的概率编程语言（如 Anglican，Church 和 Venture），分析它们的语义基础，运用测度论、随机标记转移系统和函子范畴，定义操作语义和标称语义，并证明其存在性、充分性、终止性，采用其来验证编译器优化和推理算法的正确性，研究了高阶函数上概率分布的性质。

Jan, 2016

本文通过在 terms 上创建一个 measure space，定义级别逐步逼近的连续 lambda-Calculus 的典型操作语义，并定义采样基异质的语义来实现 MCMC 的 Tracing，并证明了分布语义与集成所有 Traces 的分布具有等价性，这是第一个针对高阶函数语言 Trace MCMC 的验证正确性的证明。

Dec, 2015

我们提出一个模块化的语义计算方法，用于概率编程语言中的贝叶斯推断算法，并使用高阶函数和归纳类型等方式操纵概率程序的中间表示，定义了语义结构类及其转换的词义准则，并使用 Kock's 综合测度理论证明了一个准 Borel 同源定理。

Nov, 2017

该论文将神经网络的密度证明扩展到在概率密度函数紧致集合中的连续函数，进而给出了树形结构域的通用逼近定理，在结构化数据处理中具有重要的实际应用，这是 AutoML 范例的一个很好的例子。

Jun, 2019

研究高阶统计概率程序的微分特性，包括 SPCF、条件概率和可重复性，证实由原始函数（如解析函数）生成的几乎全是终止的 SPCF 程序的权重函数和值函数几乎全是可微的，并通过随机符号执行来推理可微性，该结果对于梯度下降推断算法的正确性需要满足权重函数的几乎全局可微性。

Apr, 2020

通过引入引伸函数，扩展一阶稳定模型语义，并将其用作定义 Answer Set Programming Modulo Theories (ASPMT) 的基础，从而实现类似 SMT 的有效一阶推理，解决包含实数的领域中的接地问题。

Jul, 2023

本文提出了一种方法，利用函数映射框架高效计算非刚性形状之间具有保方向和近似连续性的对应关系，并通过引入新的方法对初始函数映射进行改进，从而获得高质量的点对应关系。研究表明，该方法在保持连续性和覆盖率方面显著优于现有技术，并且产生的对应关系是有意义的。

Jun, 2018

本文研究如何编译具有失效、离散和连续分布的概率编程语言，并证明其正确性。通过使用标准的马尔可夫链蒙特卡罗框架对全球碳循环进行建模解决推理问题，表明本编译器大大减少了领域专家的开发工作量。

Apr, 2017

本文研究紧致拓扑空间上的功能数据和紧致度量测度空间上的结构数据的持久同调。我们探讨保留形状信号的性质的持久同调不变量的稳定性，并使用降低信号弱区域影响的度量来研究数据的持久同调不变量的连贯性和估计。我们还应用这种方法来构建紧致黎曼流形上的多尺度拓扑描述符。

Nov, 2018