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.”
■Schedule for 2025-2026 academic year (Autumn)
| Date | Speaker |
|---|---|
| 2025 Nov 6 | Qian Chen 陈谦 (Tsinghua University) |
| 2025 Nov 20 | Xi Yang 杨曦 (Tsinghua University) [Logic Reading Program] |
| 2025 Dec 11 | Weijun Yu 余伟俊 (Tsinghua University) |
| 2025 Dec 12 | Xi Yang 杨曦 (Tsinghua University) [Logic Reading Program] |
| 2025 Dec 26 | Xin Li 李鑫 (Tsinghua University) [Logic Reading Program] |
| 2026 Jan 6 | Xin Li 李鑫 (Tsinghua University) [Logic Reading Program] |
■Current Sessions
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.
