With Steve Awodey, Justyna Grudzinska, and Marek Zawadowski, I organized the workshop “New Type Theoretic Tools in Natural Language Semantics” as one of the courses at NASSLLI 2018. Reproduced here are the description and program (with slides):

New Type Theoretic Tools in Natural Language Semantics

Following the introduction of type-theoretic methods into natural language semantics (locus classicus Montague 1973), both formal natural language semantics and type theory have emerged as diverse fields of inquiry. Though simple type theory has maintained enduring popularity as a foundation for natural language semantics, further exchange of ideas between these two fields has historically been limited. However, recent years have renewed this exchange, in particular seeing the application to semantics of modern type-theoretic tools such as dependent types (from Ranta 1994), monads (from Barker 2002, Shan 2002), and comonads (from Awodey et al. 2015). This workshop will further the understanding of these tools and the development of their valuable linguistic applications.

Monads (respectively comonads) are a tool for seamlessly enriching semantic representations with extra outputs (respectively inputs). Such enrichments are integrated modularly on top of a core compositional semantics. These ‘extra outputs’ may naturally include modifications to discourse or common ground representations. This underlies the monadic approach to dynamic semantics (Charlow 2014). Monadic methods have furthermore been used for an influential analysis of quantifier scope ambiguities (Barker 2002). As for ‘extra inputs’, an important case is provided by intensional phenomena. These are modeled with semantic representations which take in ‘intensionalized’ inputs, and are thus susceptible to a comonadic analysis (Awodey et al. 2015, Zwanziger 2017).

Dependent types greatly enrich the expressive power of type theory, and have found diverse applications in semantics as a result. A key goal for the workshop is to identify and discuss common themes between these. The applications addressed in detail will include tracking anaphoric dependencies and presuppositions in discourse (Bekki 2014, 2017; Grudzinska, Zawadowski 2014, 2017), modeling lexical phenomena such as selectional restrictions and coercions (Luo 2012; Luo, Chatzikyriakidis 2017), and adjectival/adverbial modification (Luo, Chatzikyriakidis 2017). Finally, dependent types are implemented in proof assistants such as Agda, Coq, and Lean, providing a ready-made framework for computational semantics.

Program

Day 1 (Tutorials)
Welcome —Zwanziger (CMU)
Dependent Types Tutorial —Zawadowski (Warsaw)
Formal Semantics in Modern Type Theories (MTTs) —Chatzikyriakidis (Gothenburg)

Day 2 (Tutorials):
Intro. to Dependent Type Semantics —Bekki (Ochanomisu)
Intro. to Monads and Comonads —Awodey (CMU)

Day 3 (Tutorials):
Effectful Composition in Natural Language Semantics—Charlow (Rutgers) & Bumford (UCLA)

Day 4 (Talks):
Scope in Natural Language: Why Monads aren’t Enough —Barker (NYU)
Tracking Anaphors and Taking Scopes with Dependent Types —Grudzinska (Warsaw)

Day 5 (Talks):
Intensionality is Comonadic —Zwanziger (CMU)
Formal Semantics in MTTs: Playing Around with the Coq Proof Assistant —Chatzikyriakidis (Gothenburg)