{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T01:33:03Z","timestamp":1777253583565,"version":"3.51.4"},"reference-count":150,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T00:00:00Z","timestamp":1774569600000},"content-version":"unspecified","delay-in-days":85,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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\u00f6f dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant.<\/jats:p>","DOI":"10.1017\/s0960129526100516","type":"journal-article","created":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T08:09:03Z","timestamp":1774598943000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A dependently-typed calculus of event telicity and culminativity"],"prefix":"10.1017","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7609-7590","authenticated-orcid":false,"given":"Pavel","family":"Kovalev","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/05x2bcf33","id-type":"ROR","asserted-by":"publisher"}],"name":"Carnegie Mellon University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9590-3303","authenticated-orcid":false,"given":"Carlo","family":"Angiuli","sequence":"additional","affiliation":[{"name":"Indiana University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2026,3,27]]},"reference":[{"key":"S0960129526100516_ref21","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-linguistics-011718-012528"},{"key":"S0960129526100516_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-017-9246-2"},{"key":"S0960129526100516_ref36","doi-asserted-by":"publisher","DOI":"10.5617\/osla.6679"},{"key":"S0960129526100516_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63172-0_45"},{"key":"S0960129526100516_ref122","doi-asserted-by":"publisher","DOI":"10.1017\/9780511734830"},{"key":"S0960129526100516_ref91","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.020"},{"key":"S0960129526100516_ref103","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-2506-5_10"},{"key":"S0960129526100516_ref139","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511610578"},{"key":"S0960129526100516_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/BF00603391"},{"key":"S0960129526100516_ref74","first-page":"29","volume-title":"Lexical Matters","author":"Krifka","year":"1992"},{"key":"S0960129526100516_ref135","unstructured":"The Agda Development Team (2020). The Agda programming language."},{"key":"S0960129526100516_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/9781009285322"},{"key":"S0960129526100516_ref99","first-page":"15","article-title":"Temporal ontology and temporal reference","volume":"14","author":"Moens","year":"1988","journal-title":"Computational Linguistics"},{"key":"S0960129526100516_ref46","unstructured":"Coquand, T. (1992). Pattern matching with dependent types. In: Nordstr\u00f6m, B. , Petersson, K. and Plotkin, G. (eds.) Proceedings of the 1992 Workshop on Types for Proofs and Programs, 66\u201379. Chalmers University of Technology."},{"key":"S0960129526100516_ref145","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511597848"},{"key":"S0960129526100516_ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-3969-4_9"},{"key":"S0960129526100516_ref123","unstructured":"Schwarzschild, R. (2011). Stubborn distributivity, multiparticipant nouns and the count\/mass distinction. In: Proceedings of the 39th Annual Meeting of the North East Linguistic Society (NELS 39), vol. 2, Graduate Linguistics Students Association (GLSA), University of Massachusetts, 661\u2013678."},{"key":"S0960129526100516_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037383"},{"key":"S0960129526100516_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi004"},{"key":"S0960129526100516_ref109","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0960129526100516_ref81","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.1.105"},{"key":"S0960129526100516_ref40","doi-asserted-by":"crossref","unstructured":"Cockx, J. , Tabareau, N. and Winterhalter, T. (2021). The taming of the rew: A type theory with computational assumptions. In: Proceedings of the ACM on Programming Languages, 5(POPL). New York, NY: Association for Computing Machinery, Article 60, 29 p.","DOI":"10.1145\/3434341"},{"key":"S0960129526100516_ref138","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129526100516_ref4","unstructured":"Asher, N. and Luo, Z. (2013). Formalization of coercions in lexical semantics. In: Chemla, E., Homer, V. and Winterstein, G. (eds.) Proceedings of Sinn und Bedeutung, vol. 17, 63\u201380."},{"key":"S0960129526100516_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129526100516_ref127","volume-title":"Studies in Linguistics and Philosophy","author":"Smith","year":"1997"},{"key":"S0960129526100516_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85308-2_17"},{"key":"S0960129526100516_ref37","volume-title":"Formal Semantics in Modern Type Theories","author":"Chatzikyriakidis","year":"2020"},{"key":"S0960129526100516_ref117","doi-asserted-by":"publisher","DOI":"10.1002\/9781118882139.ch11"},{"key":"S0960129526100516_ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-55386-2_15"},{"key":"S0960129526100516_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48119-6_5"},{"key":"S0960129526100516_ref149","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31262-5_17"},{"key":"S0960129526100516_ref101","first-page":"189","volume-title":"Linguaggi Nella Societ\u00e0 e Nella Tecnica","author":"Montague","year":"1970"},{"key":"S0960129526100516_ref108","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139567725"},{"key":"S0960129526100516_ref114","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-36533-2"},{"key":"S0960129526100516_ref132","doi-asserted-by":"publisher","DOI":"10.15398\/jlm.v5i2.153"},{"key":"S0960129526100516_ref134","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1150-8"},{"key":"S0960129526100516_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10988-014-9162-8"},{"key":"S0960129526100516_ref31","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S. and Luo, Z. (2015). Individuation criteria, dot-types and copredication: A view from modern type theories. In: Proceedings of the 14th Meeting on the Mathematics of Language (MoL 2015), Association for Computational Linguistics.","DOI":"10.3115\/v1\/W15-2304"},{"key":"S0960129526100516_ref42","first-page":"64","volume-title":"Lecture Notes in Computer Science","author":"Cooper","year":"2011"},{"key":"S0960129526100516_ref5","unstructured":"Babonnaud, W. (2021). On the dual interpretation\u00a0of nouns as types and predicates in semantic type theories. In: Proceedings of the ESSLLI 2021 Workshop on Computing Semantics with Types, Frames and Related Structures. Utrecht, The Netherlands: Association for Computational Linguistics, 15\u201324."},{"key":"S0960129526100516_ref98","first-page":"452","volume-title":"Some Alternative Formulations of the Event Calculus","author":"Miller","year":"2002"},{"key":"S0960129526100516_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511793936"},{"key":"S0960129526100516_ref112","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780195128079.003.0003"},{"key":"S0960129526100516_ref50","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2010-351"},{"key":"S0960129526100516_ref57","volume-title":"Reference and Generality","author":"Geach","year":"1962"},{"key":"S0960129526100516_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41578-4_3"},{"key":"S0960129526100516_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236157.014"},{"key":"S0960129526100516_ref22","volume-title":"The Wiley Blackwell Companion to Semantics","author":"Champollion","year":"2020"},{"key":"S0960129526100516_ref9","first-page":"228","volume-title":"A Proof-Theoretic Analysis of Weak Crossover","author":"Bekki","year":"2023"},{"key":"S0960129526100516_ref66","first-page":"79","volume-title":"Syntax and Semantics of Dependent Types","author":"Hofmann","year":"1997"},{"key":"S0960129526100516_ref93","doi-asserted-by":"publisher","DOI":"10.1515\/9783110226614"},{"key":"S0960129526100516_ref100","volume-title":"Untersuchungen Zu Einer Konstruktiven Semantik f\u00fcr Ein Fragment Des Englischen","author":"M\u00f6nnich","year":"1985"},{"key":"S0960129526100516_ref2","unstructured":"Angiuli, C. and Gratzer, D. (2025). Principles of Dependent Type Theory (in preparation). Manuscript available at https:\/\/carloangiuli.com\/papers\/type-theory-book.pdf. Version from May 1, 2025."},{"key":"S0960129526100516_ref94","doi-asserted-by":"publisher","DOI":"10.1515\/9783110589245-008"},{"key":"S0960129526100516_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"S0960129526100516_ref26","volume-title":"Type Theory for Natural Language Semantics","author":"Chatzikyriakidis","year":"2018"},{"key":"S0960129526100516_ref45","doi-asserted-by":"publisher","DOI":"10.1002\/9781118882139.ch12"},{"key":"S0960129526100516_ref59","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/W14-1402"},{"key":"S0960129526100516_ref84","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31262-5_12"},{"key":"S0960129526100516_ref118","first-page":"97","volume-title":"The Projection of Arguments: Lexical and Compositional Factors","author":"Rappaport Hovav","year":"1998"},{"key":"S0960129526100516_ref86","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43742-1_14"},{"key":"S0960129526100516_ref6","volume-title":"Radical Pragmatics","author":"Bach","year":"1981"},{"key":"S0960129526100516_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53826-5_6"},{"key":"S0960129526100516_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-9473-7"},{"key":"S0960129526100516_ref102","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1970.tb00434.x"},{"key":"S0960129526100516_ref39","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129526100516_ref44","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780192871312.001.0001"},{"key":"S0960129526100516_ref89","unstructured":"Luo, Z. and Pollack, R. (1992). LEGO Proof Development System: User\u2019s Manual. LFCS Report ECS-LFCS-92-211, Edinburgh: Department of Computer Science, University of Edinburgh. Available at: https:\/\/www.lfcs.inf.ed.ac.uk\/reports\/92\/ECS-LFCS-92-211\/."},{"key":"S0960129526100516_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43742-1_2"},{"key":"S0960129526100516_ref72","unstructured":"Krifka, M. (1986). Nominalreferenz und Zeitkonstitution. Zur Semantik vonMassentermen, Individualtermen, Aspektklassen. PhD thesis, University of Munich, Munich."},{"key":"S0960129526100516_ref15","unstructured":"Bradley, F. and Luo, Z. (2023). A metatheoretic analysis of subtype universes. In: 28th International Conference on Types for Proofs and Programs (TYPES 2022), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik."},{"key":"S0960129526100516_ref18","volume-title":"The Logic of Decision and Action","author":"Casta\u00f1eda","year":"1967"},{"key":"S0960129526100516_ref116","volume-title":"Type-Theoretical Grammar","author":"Ranta","year":"1994"},{"key":"S0960129526100516_ref105","doi-asserted-by":"publisher","DOI":"10.1007\/BF00149015"},{"key":"S0960129526100516_ref85","doi-asserted-by":"publisher","DOI":"10.1007\/s10988-013-9126-4"},{"key":"S0960129526100516_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39998-5_10"},{"key":"S0960129526100516_ref147","doi-asserted-by":"publisher","DOI":"10.3765\/sp.11.1"},{"key":"S0960129526100516_ref16","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010648911114"},{"key":"S0960129526100516_ref136","unstructured":"The Rocq Development Team (2025). The Rocq Prover Reference Manual. Available at: https:\/\/rocq-prover.org\/refman\/."},{"key":"S0960129526100516_ref48","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198853404.001.0001"},{"key":"S0960129526100516_ref60","first-page":"37","volume-title":"Logic, Language, and Computation. TbiLLC 2015","author":"Grudzi\u0144ska","year":"2017"},{"key":"S0960129526100516_ref73","doi-asserted-by":"publisher","DOI":"10.1515\/9783110877335-005"},{"key":"S0960129526100516_ref79","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"S0960129526100516_ref54","first-page":"188","article-title":"Priznaki i tipy v teoretiko-tipovoy semantike yestestvennogo yazyka [Features and types in type-theoretical natural language semantics]","volume":"8","author":"Domanov","year":"2024","journal-title":"Filosofiya. Zhurnal Vysshey shkoly ekonomiki [Philosophy. Journal of the Higher School of Economics]"},{"key":"S0960129526100516_ref87","unstructured":"Luo, Z. (2019). MTT-Semantics is Model-Theoretic as well as Proof-Theoretic. Unpublished manuscript, 49 pp., 4 July 2019. Available at: https:\/\/www.cs.rhul.ac.uk\/~zhaohui\/BOTH.pdf."},{"key":"S0960129526100516_ref65","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780195128079.003.0002"},{"key":"S0960129526100516_ref125","volume-title":"Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia","author":"Shanahan","year":"1997"},{"key":"S0960129526100516_ref77","first-page":"302","volume-title":"Meaning, Use, and Interpretation of Language, Grundlagen der Kommunikation Und Kognition\/Foundations of Communication and Cognition","author":"Link","year":"1983"},{"key":"S0960129526100516_ref131","unstructured":"Sutton, P. R. and Filip, H. (2018). Restrictions on subkind Coercion in object mass nouns. In: Truswell, R. , Cummins, C. , Heycock, C. , Rabern, B. and Rohde, H. (eds.) Proceedings of Sinn und Bedeutung 21, Edinburgh, UK: University of Edinburgh, 1195\u20131213."},{"key":"S0960129526100516_ref126","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48317-9_17"},{"key":"S0960129526100516_ref49","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198749004.001.0001"},{"key":"S0960129526100516_ref150","first-page":"278","volume-title":"Polyadic Quantifiers on Dependent Types","author":"Zawadowski","year":"2024"},{"key":"S0960129526100516_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43742-1_4"},{"key":"S0960129526100516_ref121","doi-asserted-by":"publisher","DOI":"10.1093\/jos\/ffq007"},{"key":"S0960129526100516_ref38","first-page":"38","volume-title":"Gradability in MTT-Semantics","author":"Chatzikyriakidis","year":"2022"},{"key":"S0960129526100516_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50422-3_4"},{"key":"S0960129526100516_ref142","doi-asserted-by":"publisher","DOI":"10.2307\/2182371"},{"key":"S0960129526100516_ref13","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2000-42201"},{"key":"S0960129526100516_ref35","first-page":"43","volume-title":"Studies in Linguistics and Philosophy","author":"Chatzikyriakidis","year":"2017"},{"key":"S0960129526100516_ref130","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-linguistics-031422-113929"},{"key":"S0960129526100516_ref129","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5203-4_8"},{"key":"S0960129526100516_ref63","doi-asserted-by":"publisher","DOI":"10.1017\/S0022226722000111"},{"key":"S0960129526100516_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-014-9208-x"},{"key":"S0960129526100516_ref56","volume-title":"Logic, Language, and Meaning","author":"Gamut","year":"1990"},{"key":"S0960129526100516_ref64","first-page":"547","article-title":"On semantics","volume":"16","author":"Higginbotham","year":"1985","journal-title":"Linguistic Inquiry"},{"key":"S0960129526100516_ref69","unstructured":"Kovalev, P. (2024). Modeling Telicity With Dependent Types. PhD thesis, Indiana University, Bloomington."},{"key":"S0960129526100516_ref143","doi-asserted-by":"publisher","DOI":"10.7591\/9781501743726"},{"key":"S0960129526100516_ref124","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00036-Z"},{"key":"S0960129526100516_ref95","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P. (1975). An intuitionistic theory of types: Predicative part. In: Rose, H. E. and Shepherdson, J. C. (eds.) Logic Colloquium \u201973, vol. 80 of Studies in Logic and the Foundations of Mathematics, North-Holland, 73\u2013118.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S0960129526100516_ref137","unstructured":"Uemura, T. (2021). Abstract and Concrete Type Theories. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam."},{"key":"S0960129526100516_ref20","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198755128.001.0001"},{"key":"S0960129526100516_ref104","doi-asserted-by":"publisher","DOI":"10.1002\/9781118882139.ch18"},{"key":"S0960129526100516_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF00627432"},{"key":"S0960129526100516_ref34","unstructured":"Chatzikyriakidis, S. and Luo, Z. (2017b). Identity criteria of CNs: Quantification and copredication. In: Workshop on Approaches to Coercion and Polysemy, Oslo."},{"key":"S0960129526100516_ref92","unstructured":"Maclean, H. and Luo, Z. (2021). Subtype universes. In: de'Liguoro, U., Berardi, S. and Altenkirch, T. (eds.) 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 188. Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 9:1\u20139:16."},{"key":"S0960129526100516_ref140","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139166799"},{"key":"S0960129526100516_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/9781316418086"},{"key":"S0960129526100516_ref141","doi-asserted-by":"publisher","DOI":"10.1075\/cilt.59"},{"key":"S0960129526100516_ref51","doi-asserted-by":"publisher","DOI":"10.2307\/jj.13027259.6"},{"key":"S0960129526100516_ref1","unstructured":"Ahn, R. M. C. (2001). Agents, Objects and Events: A Computational Approach to Knowledge, Observation and Communication. Phd thesis, Eindhoven University of Technology, Eindhoven."},{"key":"S0960129526100516_ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22221-4_11"},{"key":"S0960129526100516_ref97","doi-asserted-by":"crossref","unstructured":"Mery, B. , Moot, R. and Retor\u00e9, C. (2018). Solving the individuation and counting puzzle with $\\lambda$ -DRT and MGL: If I can get a book from the library, it saves Me from needing to buy it in the bookshop. In: New Frontiers in Artificial Intelligence: JSAI-IsAI 2018 Workshops, JURISIN, AI-Biz, SKL, LENLS, IDAA, Yokohama, Japan, November 12\u201314, 2018, Revised Selected Papers, Berlin, Heidelberg: Springer-Verlag, 298\u2013312.","DOI":"10.1007\/978-3-030-31605-1_22"},{"key":"S0960129526100516_ref111","volume-title":"Events in the Semantics of English","author":"Parsons","year":"1990"},{"key":"S0960129526100516_ref10","first-page":"11","volume-title":"Studies in Linguistics and Philosophy","author":"Bekki","year":"2017"},{"key":"S0960129526100516_ref71","volume-title":"Computing Meaning","author":"Krahmer","year":"1999"},{"key":"S0960129526100516_ref119","unstructured":"Retor\u00e9, C. (2014). The montagovian generative lexicon lambda $Ty_n$ : A type theoretical framework for natural language semantics. In: Matthes, R. and Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol. 26 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany: Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 202\u2013229."},{"key":"S0960129526100516_ref110","first-page":"1","article-title":"Polysemy and co-predication","volume":"4","author":"Ortega-Andr\u00e9s","year":"2019","journal-title":"Glossa: A Journal of General Linguistics"},{"key":"S0960129526100516_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"S0960129526100516_ref82","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2009). Type-theoretical semantics with coercive subtyping. In: Semantics and Linguistic Theory 20 (SALT20), vol. 20, Vancouver: Linguistic Society of America, 38\u201356.","DOI":"10.3765\/salt.v20i0.2580"},{"key":"S0960129526100516_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30077-7_7"},{"key":"S0960129526100516_ref113","first-page":"216","volume-title":"Language Evolution and Changes in Chinese, number 26 in Journal of Chinese Linguistics Monograph Series","author":"Peck","year":"2016"},{"key":"S0960129526100516_ref76","unstructured":"Krifka, M. (2001). The mereological approach to aspectual composition. In: Handout presented at the Conference Perspectives on Aspect, University of Utrecht."},{"key":"S0960129526100516_ref58","doi-asserted-by":"crossref","unstructured":"Gilbert, G. , Cockx, J. , Sozeau, M. and Tabareau, N. (2019). Definitional proof-irrelevance without K. In: Proceedings of the ACM on Programming Languages, 3(POPL). New York, NY: Association for Computing Machinery.","DOI":"10.1145\/3290316"},{"key":"S0960129526100516_ref88","unstructured":"Luo, Z. (2021). On type-theoretical semantics of donkey anaphora. In: Logical Aspects of Computational Linguistics (LACL\u201921), Montpellier (online)."},{"key":"S0960129526100516_ref146","doi-asserted-by":"publisher","DOI":"10.1017\/9781108698283.021"},{"key":"S0960129526100516_ref128","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00063-X"},{"key":"S0960129526100516_ref120","volume-title":"Explorations in Semantics","author":"Rothstein","year":"2004"},{"key":"S0960129526100516_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/BF00133686"},{"key":"S0960129526100516_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0052155"},{"key":"S0960129526100516_ref144","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2478-4"},{"key":"S0960129526100516_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-019-09280-9"},{"key":"S0960129526100516_ref115","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9397-7_6"},{"key":"S0960129526100516_ref67","doi-asserted-by":"publisher","DOI":"10.1016\/0010-0277(91)90031-X"},{"key":"S0960129526100516_ref14","unstructured":"Boldini, P. (2001). The reference of mass terms from a type theoretical point of view. In: Proceedings of the 4th International Workshop on Computational Semantics. Tilburg."},{"key":"S0960129526100516_ref148","first-page":"174","volume-title":"Lecture Notes in Computer Science","author":"Winter","year":"2011"},{"key":"S0960129526100516_ref96","first-page":"224","volume-title":"Appositive Projection as Implicit Context Extension in Dependent Type Semantics","author":"Matsuoka","year":"2024"},{"key":"S0960129526100516_ref107","volume-title":"Commonsense Reasoning: An Event Calculus-Based Approach","author":"Mueller","year":"2014"},{"key":"S0960129526100516_ref133","unstructured":"Tenny, C. L. (1987). Grammaticalizing aspect and affectedness. PhD thesis, Massachusetts Institute of Technology, Cambridge."},{"key":"S0960129526100516_ref106","first-page":"671","volume-title":"Handbook of Knowledge Representation, Chapter 17","author":"Mueller","year":"2008"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129526100516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T00:46:34Z","timestamp":1777250794000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129526100516\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":150,"alternative-id":["S0960129526100516"],"URL":"https:\/\/doi.org\/10.1017\/s0960129526100516","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"\u00a9 The Author(s), 2026. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e9"}}