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.

翻译：本文提出一个依赖类型的跨语言框架，用于分析事件的终结性与完成性，并通过英语句子的建模示例加以说明。该框架包含两个部分：在名词性领域，我们建模名词短语的有界性及其与子类型、限定数量以及形容词修饰的关系；在动词性领域，我们定义了一个依赖事件演算，将有界受事者参与的事件建模为终结性事件，将达成内在终点的终结性事件建模为完成性事件，并考察副词修饰的影响。在两个领域中，我们特别关注相关的蕴涵关系。本框架被定义为内涵马丁-洛夫依赖类型理论的扩展，文中的规则与示例已在Agda证明助手中形式化实现。