A dependently-typed calculus of event telicity and culminativity
Pavel Kovalev, Carlo Angiuli
TL;DR
The paper develops a cross-linguistic framework for telicity and culminativity implemented in predicative intensional Martin-Löf type theory, with two integrated domains: nominal (boundedness, internal NP structure, and adjectival modification) and verbal (dependent event types indexed by actors and bounded undergoers). By treating events as dependent types and tying telicity to the boundedness of undergoers, the approach cleanly separates telicity from culminativity and supports rich entailments, including adverbial modification and state-based culminations, all formalized in Agda. Key contributions include explicit nominal infrastructure for boundedness, a dependent event calculus for telic/atelic and culminating vs non-culminating dynamics, and a formal Agda implementation that demonstrates the framework and its entailments. The work offers a principled, compositional, and machine-checkable account of telicity and culminativity with potential for cross-linguistic analysis and automated semantic inference. The framework provides a groundwork for connecting linguistic theory to set-theoretic semantics and proof assistants, enabling rigorous reasoning about complex natural-language entailments.
Abstract
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.