This course will introduce concepts and techniques from theoretical computer science and show how they can provide insight into established problems in semantics. The focus is not any particular technology or software, but a variety of conceptual/logical ideas that linguists and philosophers of language ought to know, and in some cases have unknowingly (and stumbingly) started to reinvent. Computer scientists have invested considerable ingenuity in studying the design and theoretical underpinnings of these tools, and they've made much progress that we can benefit from.
The tools we'll be introducing – mainly advanced type theories (like System Fω), monads, and continuations, though a fuller list is available at http://lambda.jimpryor.net/overview/ – aren't part of the diet of most everyday programmers, but they are prominent in academic CS, especially in the field of type theory and in work that uses "functional" programming languages like Haskell or OCaml.
The course will not presume previous experience with programming. We will, however, discuss concepts embodied in specific programming languages like the two just mentioned, and we will encourage experimentation with running, modifying, and writing computer programs.
Applications will include a detailed discussion and analysis of the formal fragment in Groenendijk, Stokhof and Veltman's 1996 paper "Coreference and Modality."