Lexical Semantics in Type Theory with Coercive Subtyping
Dept of Computer Science
Royal Holloway, Univ of London
Funded by the Leverhulme Trust (Grant
Ref: F/07-537/AJ; 147K; June 2011 -- Aug 2014)
Summary of the Project Proposal
There have been very interesting developments in lexical semantics
in the last fifteen years including, e.g., the Generative Lexicon
Theory . However, the research so far has
failed to provide an adequate formal account of the lexical
theories. Most of the employed formalisms are based on (extensions
of) the Montague grammar and unable to capture the
important linguistic phenomena satisfactorily.
The modern type theories such as [5,2] provide a
promising formalism for lexical semantics: the rich type structures
are capable to capture various sophisticated lexical phenomena. There
is a problem, though. In a type-theoretical semantics, as studied by Ranta , types are
used in a crucial way in place of the functional subsets as used in
Montague grammar, but the operations on types are rather fewer than
those on functional subsets and appear to be not enough for a formal
semantics. This has become a major obstacle in obtaining a
satisfactory type-theoretical semantics.
To solve this problem, we have conducted a preliminary study . It shows that a theory of subtyping is not
only useful but crucial in giving a natural and adequate
type-theoretical semantics and that coercive subtyping 
provides us with such a framework. The first goal of the current
project is to develop this type-theoretical approach, employing modern type
theory with coercive subtyping to obtain an adequate formal account
of lexical semantics as studied by Pustejovsky , Asher  and
In the past two decades, type theory has been applied successfully to
interactive theorem proving.
The second goal of this project is to apply the type theory based proof technology to linguistic reasoning, by designing and implementing a natural language reasoning tool based on the type-theoretical semantics, on top of an existing proof assistant. This will also open up a new research direction to apply the proof technology to computer-assisted reasoning with natural languages.
 N. Asher. Lexical Meaning in Context: A Web of Words. CUP, 2010.
 Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. OUP, 1994.
 Z. Luo. Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20),
 Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1). 1999.
 P. Martin-Lof. Intuitionistic Type Theory. Bibliopolis, 1984.
 J. Pustejovsky. The Generative Lexicon. MIT, 1995.
 A. Ranta. Type-Theoretical Grammar. OUP, 1994.
Relevant publications and documents
S. Chatzikyriakidis and Z. Luo. Natural Language Reasoning in Coq. J. of
Logic, Language and Information. 2014. (Accepted and to appear)
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
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,
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).