Preface ix

Chapter 1. Type Theories and Semantic Studies 1

1.1. Historical development of type theories 2

1.2. Foundational semantic languages 4

1.3. Montague's model-theoretic semantics 6

1.3.1. Simple type theory: a formal description 6

1.3.2. Montague semantics: examples and intensionality 9

1.4. MTT-semantics: formal semantics in modern type theories 10

1.4.1. A glance at MTT-semantics 10

1.4.2. MTTs as foundational semantic languages: historical notes 13

1.4.3. Merits of MTT-semantics 17

Chapter 2. Modern Type Theories 23

2.1. Judgments and contextual mechanisms 24

2.2. Type constructors 28

2.2.1. ¿-Types of dependent functions 28

2.2.2. ¿-types of dependent pairs 30

2.2.3. Disjoint union types, unit types and finite types 32

2.3. Universes 33

2.3.1. Prop and logical propositions 33

2.3.2. Universes in linguistic semantics 35

2.3.3. Tarski-style and Russell-style universes 37

2.4. Subtyping 38

2.5. Formal presentation of type theories with signatures 43

Chapter 3. Formal Semantics in Modern Type Theories 47

3.1. Basic linguistic categories 48

3.2. Several unique features of MTT-semantics 51

3.2.1. Common nouns as types 51

3.2.2. Subtyping in MTT-semantics 54

3.2.3. Judgmental interpretations and their propositional forms 60

3.3. Adjectival modification: a case study 65

3.3.1. Intersective adjectives 67

3.3.2. Subsective adjectives 69

3.3.3. Privative adjectives 71

3.3.4. Non-committal adjectives 72

Chapter 4. Advanced Modification 75

4.1. The data 75

4.2. Gradable adjectives 80

4.3. Gradable nouns 84

4.3.1. Gradable nouns as ¿-types 85

4.4. Multidimensional adjectives 86

4.4.1. Multidimensional adjectives: going more fine-grained 87

4.5. Adverbial modification 90

4.5.1. Veridicality 91

4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91

4.5.3. Domain, evaluative adverbs 95

4.5.4. Intensional adverbs 96

4.6. Final remarks on modification: vagueness 98

Chapter 5. Copredication and Individuation 99

5.1. Copredication and individuation: an introduction 100

5.2. Dot-types for copredication: a brief introduction 104

5.3. Identity criteria: individuation and CNs as setoids 108

5.3.1. Inheritance of identity criteria: usual cases of individuation 110

5.3.2. Generic semantics of numerical quantifiers 112

5.3.3. Copredication with quantification 113

5.3.4. Verbs plus adjectives: more on copredication with quantification 117

5.4. Concluding remarks and related work 119

Chapter 6. Reasoning and Verifying NL Semantics in Coq 127

6.1. Proof assistant technology based on MTTs 128

6.1.1. Mathematical proofs 128

6.1.2. Software verification 128

6.2. A linguist friendly introduction to Coq 129

6.2.1. Basics of Coq: types, sorts, functions 130

6.2.2. The proof engine of Coq 132

6.2.3. Useful proof tactics in Coq 135

6.2.4. Inductive types and record types 139

6.3. MTT-semantics in Coq 142

6.3.1. Adjectival and adverbial modification 143

6.3.2. Copredication and individuation in Coq 146

6.3.3. Related work 149

Chapter 7. Advanced Topics 151

7.1. Propositional forms of judgmental interpretations: formal treatment 151

7.2. Dependent event types 157

7.3. Dependent categorial grammars 163

Appendices 173

Appendix 1. Simple Type Theory C 175

Appendix 2. Type Constructors 177

Appendix 3. Prop and Logical Operators in Impredicative MTTs 181

Appendix 4. And for Coordination 183

Appendix 5. Formal System LF¿ 187

Appendix 6. Rules for Dot-Types 191

Appendix 7. Coq Codes 193

References 209

Index 225