dependent type theoretic methods in natural language semantics



A number of researchers are using dependent type theory as a formal tool to understand natural language. Some are using in particular homotopy type theory.


Papers using dependent type theory

  • René Ahn, Agents, Objects and Events: A computational approach to knowledge, observation and communication, Ph.D. dissertation, Eindhoven University, 2001.

  • Asher, N.: Lexical Meaning in Context: A Web of Words. Cambridge University Press (2011)

  • Asher, N., Luo, Z.: Formalisation of coercions in lexical semantics. In: Sinn und Bedeutung. vol. 17, pp. 63–80 (2012)

  • Daisuke Bekki: Representing anaphora with dependent types. In: Asher, N., Soloviev, S. (eds.) Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol.8535, pp. 14–29 (2014), Springer.

  • Daisuke Bekki, Asher, N.: Logical polysemy and subtyping. In: Motomura, Y., Butler, A., Bekki, D. (eds.) New Frontiers in Artificial Intelligence, Lecture Notes in Computer Science, vol. 7856, pp. 17–24. Springer (2013)

  • Daisuke Bekki, Satoh, M.: Calculating projections via type checking. In: Proceedings of TYTLES (to appear)

  • Robin Cooper, Austinian Truth, Attitudes and Type Theory, Research on Language and Computation. July 2005, Volume 3, Issue 2-3, pp 333-362 Springer

  • Chatzikyriakidis, S., Luo, Z.: Natural language inference in Coq. Journal of Logic, Language and Information 23(4), 441–480 (2014)

  • Zhaohui Luo: Type-theoretical semantics with coercive subtyping. In: Semantics and Linguistic Theory 20 (SALT 20). Vancouver (2010)

  • Zhaohui Luo: Contextual analysis of word meanings in type-theoretical semantics. In: Pogodalla, S., Prost, J.-P. (eds.) LACL 2011. LNCS, vol. 6736, pp. 159–174. Springer, Heidelberg (2011)

  • Zhaohui Luo: Common nouns as types. In: Béchet, D., Dikovsky, A. (eds.) LACL 2012. LNCS, vol. 7351, pp. 173–185. Springer, Heidelberg (2012), pdf.

  • Zhaohui Luo: Event Semantics with Dependent Types, pdf

  • Zhaohui Luo, Formal Semantics in Modern Type Theories: Is It Model-theoretic, Proof-theoretic, or Both?, pdf.

  • Koji Mineshima, A Presuppositional Analysis of Definite Descriptions in Proof Theory, New Frontiers in Artificial Intelligence Lecture Notes in Computer Science Volume 4914, 2008, pp 214-227 Springer

  • P. Piwek and E. Krahmer, ‘Presuppositions in Context: Constructing Bridges’, in Formal Aspects of Context, eds., P. Bonzon, M. Cavalcanti,and R. Nossum, volume 20 of Applied Logic Series, 85–106, Kluwer Academic Publishers, Dordrecht, (2000).

  • Aarne Ranta, Type-theoretical grammar. Oxford University Press (1994)

  • Sundholm, G.: Proof theory and meaning. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 3, pp. 471–506. Springer (1986)

  • Tanaka, R., Mineshima, K., Bekki, D.: Resolving modal anaphora in Dependent Type Semantics. In: Proceedings of LENLS11. pp. 43–56 (2014), Springer.

Papers using homotopy type theory

  • Bahramian, H., Nematollahi, N., Sabry, A.: Copredication in Homotopy Type Theory, pdf
  • David Corfield, Expressing ‘the structure of’ in homotopy type theory, webpage

A worked example, homotopy type theory in the Grammatical Framework?


  • Daisuke Bekki, Anaphora and Presuppositions in Dependent Type Semantics (Theoretical side) slides
  • Daisuke Bekki, Anaphora and Presuppositions in Dependent Type Semantics (Empirical side) slides
  • Ribeka Tanaka, Generalized Quantifiers in Dependent Type Semantics slides
  • Yusuke Kubota and Robert Levine, Scope parallelism in coordination in Dependent Type Semantics slides

Last revised on February 20, 2018 at 10:34:04. See the history of this page for a list of all contributions to it.