Stergios Chatzikyriakidis is Associate Professor in Computational Linguistics and Associate Director of the Center for Linguistic Theory and Studies in Probability at the University of Gothenburg, Sweden. He is a computational semanticist with an interest in formal semantics and formal syntax. Zhaohui Luo is Professor of Computer Science at Royal Holloway, University of London, UK. He has published extensively on type theory, including a research monograph published by Oxford University Press. His research has focused on MTT-semantics over the last decade.

• Preface ixChapter 1. Type Theories and Semantic Studies 11.1. Historical development of type theories 21.2. Foundational semantic languages 41.3. Montague’s model-theoretic semantics 61.3.1. Simple type theory: a formal description 61.3.2. Montague semantics: examples and intensionality 91.4. MTT-semantics: formal semantics in modern type theories 101.4.1. A glance at MTT-semantics 101.4.2. MTTs as foundational semantic languages: historical notes 131.4.3. Merits of MTT-semantics 17Chapter 2. Modern Type Theories 232.1. Judgments and contextual mechanisms 242.2. Type constructors 282.2.1. Π-Types of dependent functions 282.2.2. Σ-types of dependent pairs 302.2.3. Disjoint union types, unit types and finite types 322.3. Universes 332.3.1. Prop and logical propositions 332.3.2. Universes in linguistic semantics 352.3.3. Tarski-style and Russell-style universes 372.4. Subtyping 382.5. Formal presentation of type theories with signatures 43Chapter 3. Formal Semantics in Modern Type Theories 473.1. Basic linguistic categories 483.2. Several unique features of MTT-semantics 513.2.1. Common nouns as types 513.2.2. Subtyping in MTT-semantics 543.2.3. Judgmental interpretations and their propositional forms 603.3. Adjectival modification: a case study 653.3.1. Intersective adjectives 673.3.2. Subsective adjectives 693.3.3. Privative adjectives 713.3.4. Non-committal adjectives 72Chapter 4. Advanced Modification 754.1. The data 754.2. Gradable adjectives 804.3. Gradable nouns 844.3.1. Gradable nouns as Σ-types 854.4. Multidimensional adjectives 864.4.1. Multidimensional adjectives: going more fine-grained 874.5. Adverbial modification 904.5.1. Veridicality 914.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 914.5.3. Domain, evaluative adverbs 954.5.4. Intensional adverbs 964.6. Final remarks on modification: vagueness 98Chapter 5. Copredication and Individuation 995.1. Copredication and individuation: an introduction 1005.2. Dot-types for copredication: a brief introduction 1045.3. Identity criteria: individuation and CNs as setoids 1085.3.1. Inheritance of identity criteria: usual cases of individuation 1105.3.2. Generic semantics of numerical quantifiers 1125.3.3. Copredication with quantification 1135.3.4. Verbs plus adjectives: more on copredication with quantification 1175.4. Concluding remarks and related work 119Chapter 6. Reasoning and Verifying NL Semantics in Coq 1276.1. Proof assistant technology based on MTTs 1286.1.1. Mathematical proofs 1286.1.2. Software verification 1286.2. A linguist friendly introduction to Coq 1296.2.1. Basics of Coq: types, sorts, functions 1306.2.2. The proof engine of Coq 1326.2.3. Useful proof tactics in Coq 1356.2.4. Inductive types and record types 1396.3. MTT-semantics in Coq 1426.3.1. Adjectival and adverbial modification 1436.3.2. Copredication and individuation in Coq 1466.3.3. Related work 149Chapter 7. Advanced Topics 1517.1. Propositional forms of judgmental interpretations: formal treatment 1517.2. Dependent event types 1577.3. Dependent categorial grammars 163Appendices 173Appendix 1. Simple Type Theory C 175Appendix 2. Type Constructors 177Appendix 3. Prop and Logical Operators in Impredicative MTTs 181Appendix 4. And for Coordination 183Appendix 5. Formal System LFΔ 187Appendix 6. Rules for Dot-Types 191Appendix 7. Coq Codes 193References 209Index 225