Intro -- Contents -- Contributors -- Introduction: Modern Perspectives in Type Theoretical Semantics -- 1 Type Theories: Historical Development -- 2 Type Theories as Foundational Languages of Formal Semantics -- 3 Contents of the Volume -- References -- Part I Foundational Issues -- Context-Passing and Underspecification in Dependent Type Semantics -- 1 Introduction -- 1.1 Natural Language Semantics via Dependent Type Theory -- 1.2 Compositionality Problem of Discourse Anaphora -- 1.3 Partial Solutions in Dependent Type Theory -- 1.4 The Interpretation of Common Nouns in Dependent Type Theory -- 2 Verification Conditions of Discourse and Empirical Tests -- 3 Toward Dependent Type Semantics -- 3.1 Context-Passing Mechanism -- 3.2 Underspecified Terms -- 3.3 Syntactic Calculus and Semantic Composition -- 3.4 Type Checking as the Felicity Condition -- 3.5 Anaphora Resolution and Presupposition Binding -- 3.6 (In)accessibility -- 3.7 Inferences as Tests -- 4 Presuppositions as Type Inferences -- 4.1 Presupposition Phenomena -- 4.2 Projection -- 4.3 Filtering -- 4.4 Bridging Inferences and Gender Presuppositions of Pronouns -- 4.5 Factive Presupposition -- 5 Conclusion -- References -- On the Interpretation of Common Nouns: Types Versus Predicates -- 1 Introduction -- 2 Common Nouns as Types or Predicates: Different Approaches -- 2.1 Types Versus Predicates -- 2.2 Different Approaches to Interpretation of CNs -- 3 Predicational Forms of Judgements in Formal Semantics -- 3.1 Predicational Forms of Non-hypothetical Judgements -- 3.2 Predicational Forms of Negated Judgements -- 3.3 Conditionals: Predicational Forms of Hypothetical Judgements -- 4 Examples with Coq Experiments -- 4.1 General Set-Up for Predicational Forms -- 4.2 Examples with Explanations -- 5 Indexed Types for Interpretation of CNs -- 6 Concluding Remarks -- References -- Adapting Type Theory with Records for Natural Language Semantics -- 1 Rich Type Theory, Cognition and the Formal Semantics Tradition -- 2 Type Theory Without Records -- 3 Type Theory with Dependent Record Types -- 4 Dependent Types -- 5 Conclusion -- References -- Generalized Quantifiers on Dependent Types: A System for Anaphora -- 1 Unbound Anaphora -- 2 Main Features of the System -- 2.1 Context and Type Dependency -- 2.2 Many-Typed (Many-Sorted) Analysis -- 2.3 Generalized Quantifiers on Dependent Types -- 2.4 English-to-Formal Language Translation -- 3 Dynamic Extensions of Contexts -- 3.1 Maximal Anaphora to Quantifiers -- 3.2 Quantificational Subordination -- 3.3 Cumulative and Branching Continuations -- 3.4 `Donkey Anaphora'' -- 3.5 Nested Dependencies -- 3.6 Escaping Dependencies -- 3.7 Iterated `Donkey Examples'' -- 4 System - Syntax -- 4.1 Alphabet -- 4.2 Contexts -- 4.3 Type Formation: Σ-Types and Π-Types -- 4.4 Quantifier-Free Formulas -- 4.5 Quantifier Phrases -- 4.6 Packs of Quantifiers -- 4.7 Pre-chains and Chains of Quantifiers -- 4.8 Formulas, Sentences and ast-Sentences -- 4.9 Type Formation T -- 4.
