邓玉欣（上海财经大学计算机与人工智能学院）：经典-量子程序中概率行为的局部推理方法。
对于同时包含经典与量子构造的程序，验证其功能正确性是一项极具挑战性的任务。对于这类程序，由量子测量引发的概率行为与无限循环可能同时存在，使得验证工作变得非常复杂。我们引入分布公式来刻画概率特性，并受到分离逻辑的启发，提出了一种新型量子霍尔逻辑系统，用于对概率行为进行局部推理。我们证明了该逻辑系统中各项推理规则相对于一种指称语义的可靠性。为展示该逻辑系统的有效性，我们对HHL算法、Shor 算法等重要量子算法的正确性进行了完整的形式化验证。此外，我们将该逻辑系统嵌入到定理证明器Coq中，由此构建的逻辑框架能够有效支持经典-量子程序的半自动化推理。
王彦晶（北京大学哲学系）：Assignment Operators as Bridges.
The assignment operator, [x := t], captures one of the most fundamental operations in computation: assigning the value of a term to a variable. Its introduction to logic dates back to the early days of Dynamic Logic, where it was essential for formalizing programs and reasoning about their correctness. This talk will survey a growing body of recent research demonstrating that variants of this seemingly simple operator have applications extending far beyond program verification. I will show how these generalized forms of assignment can act as powerful “bridges” between paradigms in philosophical logic, particularly in first-order modal logic and epistemic logic. In doing so, the assignment operators render previously opaque logical expressions transparent, break the implicit assumptions, and help strike a balance between expressivity and complexity.
杨 跃（新加坡国立大学数学系）：什么是有穷类型上的可计算性？
哥德尔曾经试图利用有穷类型上的可计算泛函来证明经典数论的一致性。在他看来，可计算泛函这样的抽象概念可以被视为有穷主义的，尽管它不是希尔伯特意义上的有穷主义，见哥德尔[1972] “On an extension of finitary mathematics which has not yet been used”。在[1972] 文中，哥德尔在对可计算泛函的描述中用了“well-defined mathematical procedure”这一概念，然而他并没有给出精确的定义，仅仅说到：
The phrase “well-defined mathematical procedure” is to be accepted as having a clear meaning without any further explanation.
本报告的主要内容是试图给有穷类型上的可计算性下一个严格的定义，并将它与经典的可计算性概念作比较。
（This talk is based on joint work with Zekun Jia from National University of Singapore, Keng Meng Ng from Nanyang Technological University, Singapore and Nazanin Tavana from Amir Kabir University, Iran.）