

Dependent types for pragmatics
pp. 123-139
in: Juan Redmond, Olga Pombo Martins, Angel Fernández (eds), Epistemology, knowledge and the impact of interaction, Berlin, Springer, 2016Abstract
In this paper, we present an extension to Martin-Löf's Intuitionistic Type Theory which gives natural solutions to problems in pragmatics, such as pronominal reference and presupposition. Our approach also gives a simple account of donkey anaphora without resorting to exotic scope extension of the sort used in Discourse Representation Theory and Dynamic Semantics, thanks to the proof-relevant nature of type theory.