Types of lexical semantics
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 others.
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), Vancouver. 2010.
 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.