The course concentrates on the use of constructive type theories to the study of natural language semantics. It presents an alternative language to be used in representing the semantics of NL based on the notion of proof, rather than the notion of truth with respect to a model as standard in classic Montague Semantics.
The course syllabus can be found here.