我们在 Coq 证明助手中开发了在归纳构造计算（CIC）中的合成 oracle 可计算性和 Turing 约简的概念，并使用连续函数的顺序连续性来描述有效拓扑中基于连续函数的定义。

Jul, 2023

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

Nov, 2017

介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。

May, 2023

该研究提出类型理论是理解人类如何进行新颖问题思考、解释和猜测的核心组成部分，并以三个实证性观察来证明这一观点：学习和推论的自适应性限制、人们在不可能性和不太可能性之间区分的能力以及人类在不同层次的抽象概念上进行推理的能力。

Oct, 2022

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

Jan, 2017

开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。

Oct, 2000

本论文提出了一种基于同调理论的函数同之间的复杂性分离，并利用组合和同调交换代数及 Stanley-Reisner 理论发展了该基础理论，并推导出关于多项式阈值函数的最大定理，并给出了同调 Farkas 引理，以及一些关注的应用实例。

Jan, 2017

研究拓扑量子场论，借鉴高维代数中 n - 范畴和 n - 向量空间等概念，提出了一种适用于 n 维 TQFT 描述的 n - 范畴定义，并阐述描述 n 维 TQFT 的 n - 范畴表示的计划，包括 n - 分类变形量子化和量子双重构造等方面。

Mar, 1995

本研究探讨在数学中的程序抽象结构，定案例研究并且说明通过 Peano 定理证明环境和可重用抽象的能力，加上恰当的教学大纲，是保障自动化数学推理的长期文化传播的有效方法。

Nov, 2022

本文定义了直觉主义版本的计算树逻辑，解释了直觉主义逻辑的语义特征，并研究了其在形式验证中的应用，进而定义了直觉主义版本的 CTL 的语法和语义，并研究了该逻辑的一些简单性质。最后，我们证明了在我们定义的直觉主义版本的 CTL 中，一些 CTL 的不动点公理是无效的。

Oct, 2023