This is an invited talk by Prof. Zhaohui Luo, Royal Holloway, University of London. (email: zhaohui.luo at hotmail.co.uk)

Abstract

This talk consists of two parts. In Part I, I’ll introduce modern type theories, as studied by Martin-Löf and others [6, 2, 3, 5], briefly discussing their historical development, meaning-theoretic and meta-theoretic studies and employment in proof technology. Then, in Part II, I’ll give an overview of the following two applications of type theory:

  • Univalent foundations of mathematics, as proposed by Voevodsky [10] and studied formally in homotopy type theory [8]. The new framework provides a fresh look at foundational issues, covering both traditional set-theoretical mathematics and new higher-dimensional mathematics and providing a good basis for computer-assisted proof development.
  • Natural language semantics in modern type theories (MTT-semantics for short) [9, 4, 1]. Thanks to its recent development [1, 5], MTT-semantics has become a full-blown alternative to the traditional formal semantics (Montague semantics [7]), with attractive features and a promising future.

If time permits, I’ll also discuss some ongoing research topics in both of the above fields, albeit only briefly.

[1] S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley/ISTE, 2020. [2] T. Coquand and G. Huet. The calculus of constructions. Info. & Comp., 76(2/3), 1988. [3] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford Univ. Press, 1994. [4] Z. Luo. Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6):491–513, 2012. [5] Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press, 2024. (In Chinese). [6] P. Martin-L ̈of. Intuitionistic Type Theory. Bibliopolis, 1984. [7] R. Montague. Formal Philosophy. Yale University Press, 1974. Collected papers edited by R. Thomason. [8] The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. 2013. [9] A. Ranta. Type-Theoretical Grammar. Oxford University Press, 1994. [10] V. Voevodsky. An experimental library of formalized mathematics based on univalent foundations. Mathematical Structures in Computer Science, 25:1278–1294, 2015.

Venue information

The talk will be conducted via Zoom. All are welcome to join.

Topic: HKU PL Group Seminar
Time: May 15, 2024 08:00 PM Hong Kong SAR

Join Zoom Meeting
https://hku.zoom.us/j/99574409474?pwd=aHRIbjE1MHJlODVPZlpadHpGdFN6UT09

Meeting ID: 995 7440 9474
Password: 317826