To promote interdisciplinary interaction between different faculty members and students on the campus, a weekly meeting has been organized by our postdoc Jialiang Yan since September 2023, called Tsing Ch’a Sessions (清茶会). Its slogan “know thyself and let others know you better.”
■Current Sessions
2026 Apr 9 14:00-15:30 Wenlong Zheng (郑文龙, Tsinghua University) Nonmonotonicity and Actual Causation: The Theory of Bochman’s Causal Calculus
Causality is a fundamental concept in reasoning, yet capturing its exact formal semantics has historically posed a challenge for standard deductive systems. In his 2021 book A Logical Theory of Causality, Alexander Bochman develops a causal calculus based on rules of the form A\Rightarrow B (“A causes B”), situated within a nonmonotonic reasoning framework. By treating causal rules as default assumptions, we will see how causal reasoning emerges as a special instance of nonmonotonic reasoning developed within the knowledge representation and symbolic branches of artificial intelligence.
In this talk, we will first introduce the basic techniques of Bochman’s causal calculus. Second, we will briefly contrast this rule-based logical framework with the standard structural equation modeling (SEM) approach. Finally, the main focus of the talk will be applying this calculus to formalize actual causation.
2026 Feb 26 14:00-15:30 Haoxuan Yin (尹昊萱, University of Oxford) Modal Logic as a Type System for Metaprogramming
Metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of imperative features, ensuring program safety is challenging, as free variables can be passed around in references. In this talk, I present Layered Modal ML (LMML), a metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types (Hu & Pientka, ESOP 2024) to track and reason about free variables in code explicitly. A contextual modal type \Box(\Gamma\vdash T) reads “a piece of code of type T with free variables \Gamma.” If time permits, I will also talk about using operational game semantics to model program equivalences in LMML, and how this tool can be used to verify faithfulness in metaprogramming-based program optimisations.
This is joint work with Andrzej Murawski and Luke Ong. The full version of the paper can be found at https://arxiv.org/abs/2602.03033. The talk will not suppose any prior knowledge of programming language theory, but familiarity with statically typed programming languages such as C++ or Java would be helpful.
■Past Sessions
Click HERE to check the past sessions.
Click HERE to check the past sessions from 2025.
