2 papers
cs.CL2026
A dependently-typed calculus of event telicity and culminativity
Pavel Kovalev, Carlo Angiuli
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 se…
cs.LO2025
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…