Reference. A dependently-typed calculus of event telicity and culminativity
We present a dependently-typed cross-linguistic framework for analyzing the telicity and culminativity of events, accompanied by examples of using our framework to model English sentences. Our framework consists of two parts. In the nominal domain, we model the boundedness of noun phrases and its relationship to subtyping, delimited quantities, and adjectival modification. In the verbal domain, we define a dependent event calculus, modeling telic events as those whose undergoer is bounded, culminating events as telic events that achieve their inherent endpoint, and consider adverbial modification. In both domains, we pay particular attention to associated entailments. Our framework is defined as an extension of intensional Martin-Löf dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant.
Cite
Cites 145 works (2 here)
With notes (2)
Syntax and semantics of dependent types Hofmann_1997
External (143)
- Types and the Structure of Meaning (2025)
- Principles of Dependent Type Theory (in preparation) (2025)
- The Rocq Prover Reference Manual (2025)
- Priznaki i tipy v teoretiko-tipovoy semantike yestestvennogo yazyka [Features and types in type-theoretical natural language semantics] (2024)
- Polyadic Quantifiers on Dependent Types (2024)
- Appositive Projection as Implicit Context Extension in Dependent Type Semantics (2024)
- Modeling Telicity With Dependent Types (2024)
- A Proof-Theoretic Analysis of Weak Crossover (2023)
- From Perception to Communication (2023)
- Types and Type Theories in Natural Language Analysis (2023)
- The Cambridge Handbook of Role and Reference Grammar (2023)
- A metatheoretic analysis of subtype universes (2023)
- Gradability in MTT-Semantics (2022)
- Telicization in Mandarin Chinese (2022)
- Mereology (2021)
- The Lean 4 Theorem Prover and Programming Language (2021)
- Events in Semantics (2021)
- On the dual interpretation of nouns as types and predicates in semantic type theories (2021)
- On type-theoretical semantics of donkey anaphora (2021)
- Abstract and Concrete Type Theories (2021)
- The taming of the rew: a type theory with computational assumptions (2020)
- Formal Semantics in Modern Type Theories (2020)
- Foundations of the Theory of Parthood (2020)
- Distributivity, collectivity, and cumulativity (2020)
- Modal Homotopy Type Theory (2020)
- The Agda programming language (2020)
- Distributivity in Formal Semantics (2019)
- Solving the Individuation and Counting Puzzle with λ-DRT and MGL (2019)
- Polysemy and co-predication (2019)
- A Scope-Taking System with Dependent Types and Continuations (2019)
- Definitional proof-irrelevance without K (2019)
- Inverse Linking, Possessive Weak Definites and Haddock Descriptions: A Unified Dependent Type Account (2019)
- MTT-Semantics is Model-Theoretic as well as Proof-Theoretic (2019)
- Identity Criteria of Common Nouns and dot-types for Copredication (2018)
- Type Theory for Natural Language Semantics (2018)
- Symmetric predicates and the semantics of reciprocal alternations (2018)
- Restrictions on subkind Coercion in object mass nouns (2018)
- Adjectival and Adverbial Modification: The View from Modern Type Theories (2017)
- Semantics for Counting and Measuring (2017)
- Dependent Event Types (2017)
- Factivity and presupposition in Dependent Type Semantics (2017)
- Whence long-distance indefinite readings? Solving Chierchia's puzzle with dependent types (2017)
- Adapting Type Theory with Records for Natural Language Semantics (2017)
- Parts of a Whole (2017)
- Context-passing and underspecification in dependent type semantics (2017)
- Identity criteria of CNs: Quantification and copredication (2017)
- On the interpretation of common nouns: Types versus predicates (2017)
- Mereology (2016)
- Proof Assistants for Natural Language Semantics (2016)
- Language Evolution and Changes in Chinese, number 26 in Journal of Chinese Linguistics Monograph Series (2016)
- Constructive Type Theory (2015)
- A Type-Logical Account of Quantification in Event Semantics (2015)
- The interaction of compositional semantics and event semantics (2015)
- Individuation Criteria, Dot-types and Copredication: A View from Modern Type Theories (2015)
- Type Theory with Records for Natural Language Semantics (2015)
- Natural Logic (2015)
- Type Theory and Formal Proof (2014)
- System with Generalized Quantifiers on Dependent Types for Anaphora (2014)
- Formal Semantics in Modern Type Theories: Is It Model-Theoretic, Proof-Theoretic, or Both? (2014)
- Representing Anaphora with Dependent Types (2014)
- Adverbs in a Modern Type Theory (2014)
- Natural Language Inference in Coq (2014)
- Commonsense Reasoning: An Event Calculus-Based Approach (2014)
- The montagovian generative lexicon lambda Tyn : A type theoretical framework for natural language semantics (2014)
- Coercive subtyping: Theory and implementation (2013)
- An Account of Natural Language Coordination in Type Theory with Coercive Subtyping (2013)
- Adjectives in a Modern Type-Theoretical Setting (2013)
- Formalization of coercions in lexical semantics (2013)
- On Link’s “The Logical Analysis of Plurals and Mass Terms: A Lattice-theoretical Approach” (2012)
- Dot-types and Their Implementation (2012)
- Common Nouns as Types (2012)
- Formal semantics in modern type theories with coercive subtyping (2012)
- Lexical Meaning in Context (2011)
- Contextual Analysis of Word Meanings in Type-Theoretical Semantics (2011)
- Copredication, quantification and frames (2011)
- Stubborn distributivity, multiparticipant nouns and the count/mass distinction (2011)
- Event semantics and abstract categorial grammar (2011)
- Modeling Contexts with Dependent Types (2010)
- Counting and the Mass/Count Distinction (2010)
- Type-theoretical semantics with coercive subtyping (2010)
- Handbook of Knowledge Representation, Chapter 17 (2008)
- Exploring the Syntax-Semantics Interface (2005)
- Records and Record Types in Semantic Theory (2005)
- Some Alternative Formulations of the Event Calculus (2002)
- An Implementation of LF with Coercive Subtyping & Universes (2001)
- Coercion completion and conservativity in coercive subtyping (2001)
- Agents, Objects and Events: A Computational Approach to Knowledge, Observation and Communication (2001)
- The reference of mass terms from a type theoretical point of view (2001)
- The mereological approach to aspectual composition (2001)
- Underlying States and Time Travel (2000)
- On Events in Linguistic Semantics (2000)
- Formalizing Context in Intuitionistic Type Theory (2000)
- Presuppositions in Context: Constructing Bridges (2000)
- Coercive Subtyping (1999)
- The Event Calculus Explained (1999)
- Presupposition projection as proof construction (1999)
- The Origins of Telicity (1998)
- The Projection of Arguments: Lexical and Compositional Factors (1998)
- Coercive subtyping in type theory (1997)
- The parameter of aspect (1997)
- Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia (1997)
- Syntax: Structure, Meaning, and Function (1997)
- Vagueness and type theory (1997)
- The proper treatment of measuring out, telicity, and perhaps even quantification in english (1996)
- A circumscriptive calculus of events (1995)
- Aspectual Roles and the Syntax-Semantics Interface (1994)
- Type-Theoretical Grammar (1994)
- Computation and Reasoning (1994)
- A Theory of Aspectuality (1993)
- Pattern matching with dependent types (1992)
- Thematic relations as links between nominal reference and temporal constitution (1992)
- LEGO Proof Development System: User’s Manual (1992)
- Parts and boundaries (1991)
- Programming in Martin-Löf’s Type Theory (1990)
- Logic, Language, and Meaning (1990)
- Events in the Semantics of English (1990)
- Nominal Reference, Temporal Constitution and Quantification in Event Semantics (1989)
- Temporal ontology and temporal reference (1988)
- The Calculus of Constructions (1988)
- Event Structure (1988)
- Mass terms and quantification (1987)
- Grammaticalizing aspect and affectedness (1987)
- A logic-based calculus of events (1986)
- Generalised algebraic theories and contextual categories (1986)
- Proof Theory and Meaning (1986)
- The algebra of events (1986)
- Nominalreferenz und Zeitkonstitution (1986)
- Untersuchungen Zu Einer Konstruktiven Semantik für Ein Fragment Des Englischen (1985)
- Meaning, Use, and Interpretation of Language, Grundlagen der Kommunikation Und Kognition/Foundations of Communication and Cognition (1983)
- On time, tense, and aspect: An essay in English metaphysics (1981)
- Word Meaning and Montague Grammar (1979)
- Events, processes, and states (1978)
- An Intuitionistic Theory of Types: Predicative Part (1975)
- The Proper Treatment of Quantification in Ordinary English (1973)
- On the Compositional Nature of the Aspects (1972)
- English as a formal language (1970)
- Universal grammar (1970)
- Comments (in The Logic of Decision and Action) (1967)
- Linguistics in Philosophy (1967)
- The Logical Form of Action Sentences (1967)
- Reference and Generality (1962)
- Verbs and Times (1957)
- A formulation of the simple theory of types (1940)