Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis

      1  Cover

      2  Title page

      3  Copyright

      4  Preface

      5  1 Type Theories and Semantic Studies 1.1. Historical development of type theories 1.2. Foundational semantic languages 1.3. Montague’s model-theoretic semantics 1.4. MTT-semantics: formal semantics in modern type theories

      6  2 Modern Type Theories 2.1. Judgments and contextual mechanisms 2.2. Type constructors 2.3. Universes 2.4. Subtyping 2.5. Formal presentation of type theories with signatures

      7  3 Formal Semantics in Modern Type Theories 3.1. Basic linguistic categories 3.2. Several unique features of MTT-semantics 3.3. Adjectival modification: a case study

      8  4 Advanced Modification 4.1. The data 4.2. Gradable adjectives 4.3. Gradable nouns 4.4. Multidimensional adjectives 4.5. Adverbial modification 4.6. Final remarks on modification: vagueness

      9  5 Copredication and Individuation 5.1. Copredication and individuation: an introduction 5.2. Dot-types for copredication: a brief introduction 5.3. Identity criteria: individuation and CNs as setoids

      10  6 Reasoning and Verifying NL Semantics in Coq 6.1. Proof assistant technology based on MTTs 6.2. A linguist friendly introduction to Coq 6.3. MTT-semantics in Coq

      11  7 Advanced Topics 7.1. Propositional forms of judgmental interpretations: formal treatment 7.2. Dependent event types 7.3. Dependent categorial grammars

      12  Appendices Appendix 1: Simple Type Theory C A1.1. Inference rules of C A1.2. Logical operators in C Appendix 2: Type Constructors A2.1. Π-types A2.2. Σ-types A2.3. Disjoint union types A2.4. The unit type and finite types Appendix 3: Prop and Logical Operators in Impredicative MTTs A3.1. Prop A3.2. Logical operators Appendix 4: And for Coordination Appendix 5: Formal System LF_Δ A5.1. LF_Δ A5.2. Σ-types in LF_Δ Appendix 6: Rules for Dot-Types Appendix 7: Coq Codes A7.1. Some basic ontology and subtyping declarations A7.2. Simple homonymy by overloading in coercive subtyping A7.3. Intersective and subsective adjectives A7.4. Privative adjectives A7.5. Multidimensional adjectives A7.6. Gradable adjectives A7.7. Veridical adverbs A7.8. Manner adverbs A7.9. Individuation

      13  References

      14  Index

      15  End User License Agreement

      1 PrefaceFigure P.1. Dependency diagram for reading

      2 Chapter 2Figure 2.1.