Leverhulme Project

Lexical Semantics in Type Theory with Coercive Subtyping

Zhaohui Luo
Dept of Computer Science
Royal Holloway, Univ of London

Funded by the Leverhulme Trust (Grant Ref: F/07-537/AJ; 147K)

Summary of the Project Proposal

Relevant publications and documents

  • Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press. 2024.
  • Z. Luo. Common Nouns as Types: Higher Inductive Types in Type-Theoretical Semantics. Invited talk at Logic Colloquium 2024, Gothenburg, Sweden. June 2024.
  • Z. Luo. Advanced Topics in Formal Semantics Based on Modern Type Theories. Advanced Course in Language & Logic at ESSLLI 2023. Ljubljana, Slovenia. August 2023.
  • T. Xue, Z. Luo and S. Chatzikyriakidis. Propositional Forms of Judgemental Interpretations. J of Logic, Language and Information, 32(4). 2023.
  • Z. Luo. Universes in Type-Theoretical Semantics. Invited talk at Logic and Algorithms in Computational Linguistics 2021 (LACompLing21). Montpellier (online), Dec. 2021. [pdf-file of the slides available]
  • Z. Luo, Y. Shi and T. Xue. A semantic analysis of adjectival modification in modern type theories. Studies in Logic, 15(2). 2022.
  • Z. Luo. On Type-Theoretical Semantics of Donkey Anaphora. Logical Aspects of Computational Linguistics (LACL21). Montpellier (online), 2021. (An earlier version of the paper, titled "Donkey Anaphora: Type-Theoretic Semantics with Both Strong and Weak Sums", was read in Computing Semantics with Types, Frames and Related Structures 2021 (ESSLLI 2021 Workshop CSTFRS21).)
  • H. Maclean and Z. Luo. Subtype universes. Post-proceedings of the 26th Inter. Conf. on Types for Proofs and Programs (TYPES20). Leibniz International Proceedings in Informatics, Vol. 188. 2021. (The extended abstract in the TYPES20 conference is also available.)
  • S. Chatzikyriakidis and Z. Luo. Gradability in MTT-Semantics. Post-proceedings of the 13th Inter. Tbilisi Symposium on Language, Logic and Computation (TbiLLC 2019), LNCS 13206. 2021.
  • S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley/ISTE. 2020. (ISBN 978-1-78630-128-4)
  • Z. Luo. Proof Irrelevance in Type-Theoretical Semantics. Logic and Algorithms in Computational Linguistics 2018 (LACompLing2018), Studies in Computational Intelligence 860, pp1-15. Springer. 2019. (An earlier short paper titled MTT-semantics in Martin-Lof's Type Theory with HoTT's Logic appeared in the initial proceedings of LACompLing 2018. Stockholm, 2018.)
  • Z. Luo. MTT-semantics is model-theoretic as well as proof-theoretic. Manuscript (49pp). July 2019.
  • Z. Luo and S. Soloviev. Dependent Event Types in Event Semantics. TYPES 2019. Oslo, June 2019.
  • Z. Luo. Formal Semantics in Modern Type Theories: An Overview. Invited talk at LACompLing 2018, Stockholm, Sweden (also for the Third Conference on Proof-Theoretic Semantics (PTS19) at Tubingen and TYPES 2018 at Braga). (Also available: LACompLing18 slides and PTS19 slides)
  • S. Chatzikyriakidis and Z. Luo. From Montague Semantics to Modern Type Theories: A Meaningful Comparison. Advanced Course in Language & Logic at ESSLLI 2019. Riga, Latvia. 2019.
  • S. Chatzikyriakidis and Z. Luo. Identity Criteria of Common Nouns and Dot-Types for Copredication. Oslo Studies of Language 10(2). 2018.
  • Z. Luo. Substructural Calculi with Dependent Types. Linearity & TLLA (affiliaed with FLoC), Oxford. 2018.
  • T. Xue, Z. Luo and S. Chatzikyriakidis. Propositional Forms of Judgemental Interpretations. NLCS18 (affiliated with FLoC), Oxford. 2018.
  • S. Chatzikyriakidis and Z. Luo. Identity Criteria of CNs: Quantfication and Copredication. Workshop on Approaches to Coercion and Polysemy. Oslo, 2017.
  • Z. Luo. Modern Type Theories for Natural Language Semantics. Introductory course at ESSLLI 2017, Toulouse, France. July 2017.
  • Z. Luo and S. Soloviev. Dependent event types. Proc of the 24th Workshop on Logic, Language, Information and Computation (WoLLIC'17), LNCS 10388. London, 2017. (An abstract of the paper has appeared in Proc of LACL 2016.)
  • S. Chatzikyriakidis and Z. Luo. Adjectival and Adverbial Modification: The View from Modern Type Theories. Journal of Logic, Language and Information 26(1), 2017.
  • Z. Luo and S. Soloviev. Dependent event types (abstract), Logical Aspects of Computational Linguistics 2016 (LACL 2016). 2016. (Longer version of the paper is available here.)
  • S. Chatzikyriakidis and Z. Luo. Proof Assistants for Natural Language Semantics. Logical Aspects of Computational Linguistics 2016 (LACL 2016), Nancy. 2016.
  • S. Chatzikyriakidis and Z. Luo (eds.). Modern Perspectives in Type Theoretical Semantics. Studies in Linguistics and Philosophy, Springer. 2017.
  • Z. Luo. A Lambek Calculus with Dependent Types. TYPES 2015. Tallinn, May 2015.
  • S. Chatzikyriakidis and Z. Luo. Using Signatures in Type Theory to Represent Situations. T. Murata, K. Mineshima and D. Bekki (eds). New Frontiers in Artificial Intelligence - JSAI-isAI 2014 Workshops in Japan (LENLS, JURISIN and GABA), Revised Selected Papers. LNCS 9067, 2015.
  • S. Chatzikyriakidis and Z. Luo. Individuation Criteria, Dot-types and Copredication: A View from Modern Type Theories. Proc of the 14th Inter. Conf. on Mathematics of Language, Chicago, 2015.
  • S. Chatzikyriakidis and Z. Luo. Natural Language Inference in Coq. Journal of Logic, Language and Information, 23(4). 2014.
  • Z. Luo. Formal Semantics in Modern Type Theories: Is It Model-theoretic, Proof-theoretic, or Both? Invited talk at Logical Aspects of Computational Linguistics 2014 (LACL 2014), Toulouse. LNCS 8535. 2014. [Slides available]
  • S. Chatzikyriakidis. Adverbs in a Modern Type Theory. LACL 2014, LNCS 8535. 2014.
  • G. Lungu and Z. Luo. Monotonicity Reasoning in Formal Semantics Based on Modern Type Theories. LACL 2014, LNCS 8535. 2014.
  • S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories: Theory and Implementation. Advanced course at ESSLLI 2014, Tubingen, Germany. August 2014. [Lecture slides available]
  • S. Chatzikyriakidis and Z. Luo. Natural Language Reasoning Using Proof-assistant Technology: Rich Typing and Beyond. EACL Workshop on Type Theory and Natural Language Semantics (TTNLS), Goteborg, 2014.
  • S. Chatzikyriakidis and Z. Luo. Adjectives in a Modern Type-Theoretical Setting. The 18th Conf. on Formal Grammar, Dusseldorf. LNCS 8036. 2013.
  • Z. Luo. Formal Semantics in Modern Type Theories with Coercive Subtyping. Linguistics and Philosophy, 35(6). 2012.
  • N. Asher and Z. Luo. Formalisation of coercions in lexical semantics. Sinn und Bedeutung 17, Paris. 2012. [abstract also available]
  • S. Chatzikyriakidis and Z. Luo. An Account of Natural Language Coordination in Type Theory with Coercive Subtyping. Constraint Solving and Language Processing 2012, LNCS 8114. 2013.
  • Z. Luo. Common nouns as types. LACL'12, LNCS 7351. 2012.
  • T. Xue and Z. Luo. Dot-types and their implementation. LACL'12, LNCS 7351. 2012.
  • Z. Luo. Notes and slides at ESSLLI 2011, Ljubljana, Slovenia (for a course on Lexical Semantics, taught together with Prof Nicholas Asher)
  • Z. Luo. Contextual analysis of word meanings in type-theoretical semantics. Logical Aspects of Computational Linguistics (LACL'2011). LNAI 6736, 2011.
  • Z. Luo. Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver. 2010.
  • Z. Luo and P. Callaghan. Coercive subtyping and lexical semantics (extended abstract). Logical Aspects of Computational Linguistics (LACL'98). 1998.