Order:
  1.  34
    Formal Semantics in Modern Type Theories with Coercive Subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.
    In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in making type theories (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  2.  33
    Natural Language Inference in Coq.Stergios Chatzikyriakidis & Zhaohui Luo - 2014 - Journal of Logic, Language and Information 23 (4):441-480.
    In this paper we propose a way to deal with natural language inference by implementing Modern Type Theoretical Semantics in the proof assistant Coq. The paper is a first attempt to deal with NLI and natural language reasoning in general by using the proof assistant technology. Valid NLIs are treated as theorems and as such the adequacy of our account is tested by trying to prove them. We use Luo’s Modern Type Theory with coercive subtyping as the formal language into (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  3.  28
    Coercion Completion and Conservativity in Coercive Subtyping.Sergei Soloviev & Zhaohui Luo - 2001 - Annals of Pure and Applied Logic 113 (1-3):297-322.
    Coercive subtyping offers a general approach to subtyping and inheritance by introducing a simple abbreviational mechanism to constructive type theories. In this paper, we study coercion completion in coercive subtyping and prove that the formal extension with coercive subtyping of a type theory such as Martin–Löf's type theory and UTT is a conservative extension. The importance of coherence conditions for the conservativity result is also discussed.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  4.  6
    Adjectival and Adverbial Modification: The View From Modern Type Theories.Stergios Chatzikyriakidis & Zhaohui Luo - 2017 - Journal of Logic, Language and Information 26 (1):45-88.
    In this paper we present a study of adjectival/adverbial modification using modern type theories, i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented given their proof-theoretic nature. In MTT-semantics, common (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  5.  8
    Classical Predicative Logic-Enriched Type Theories.Robin Adams & Zhaohui Luo - 2010 - Annals of Pure and Applied Logic 161 (11):1315-1345.
    A logic-enriched type theory is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named and , which we claim correspond closely to the classical predicative systems of second order arithmetic and . We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography