Keynote Speaker:

Luo Zhaohui is Professor of the Department of Computer Science at Royal Holloway, University of London. He studied at the National University of Defense Technology and obtained his PhD from the University of Edinburgh, UK in 1990. He then held positions at the University of Edinburgh, Durham University and the University of London.

Devoting his entire career to the research of modern type theories and their applications, he is recognized as one of the academic leaders in this field with remarkable research achievements. His original works include Calculation and Reasoning (published by Oxford University Press in 1994), which explores unified type theory; Formal Semantics Based on Modern Type Theory (published by Wiley in 2020), which focuses on natural language semantics; and his Chinese monograph Modern Type Theories: Their Development and Applications (published by Tsinghua University Press in 2024).

Main Content:

This lecture introduces modern type theory developed by Martin-Löf and other scholars, with a brief discussion of its development, basic structure, metatheory and applications. (For a Chinese introduction to this theory, please refer to the book Modern Type Theories: Their Development and Applications.)

Regarding the applications of modern type theory, the lecture highlights formal semantics of natural language based on this theory—a rapidly developing and increasingly mature field that boasts distinct advantages over traditional Montague semantics and has promising prospects. If time permits, the lecture will also briefly discuss the applications of modern type theory in related fields such as the foundations of mathematics, formalized reasoning and interactive theorem proving in computer science.

Time:

December 10, 2025 (Wednesday), 16:20

Location:

Coffee Beanery

Organizer:

Advanced Institute of Humanities and Social Sciences (AI-HSS)