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)

### Relevant publications and documents

Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press. 2024.
(ISBN: 9787302660354)
Z. Luo. Common Nouns as Types: Higher Inductive Types in Type-Theoretical Semantics.
Invited talk at Logic Colloquium 2024, Gothenburg, Sweden. June 2024.
[slides available]
F. Bradley and Z. Luo. Representing Temporal Operators with Dependent Event Types.
Extended abstract, TYPES24, Copenhagen, 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.