In this talk, I will provide a comprehensive overview of Dependent Type Semantics (DTS), a proof-theoretic approach to natural language semantics based on dependent type theory. DTS marks a departure from the traditional model-theoretic semantic frameworks that have long been the standard, such as Montagovian intensional logic, discourse representation theory, and dynamic semantics.

The key distinguishing feature of DTS is its ability to unify analyses of linguistic phenomena such as anaphora and presupposition through the process of type checking and proof search. This is consistent with the “presupposition is anaphora” paradigm that is widely discussed and analyzed in semantic studies.

DTS computes the meaning of a given sentence through the principle of compositionality, coupled with the mechanism called “unspecified types,” which correspond to open proofs in proof assistants. This establishes a new correspondence between the meaning of natural language and type theory, shedding new light on both fields.

I will also reflect on the extensive research and developments over the past decade. This will shed light on the future prospects of DTS and provide insights into its potential applications in computational linguistics.