Forthcoming lecture at ESSLLI 2012 in Opole

Proofs, models and categories for type theory,

with selected applications to natural language semantics


Christian Retoré (Univ. Bordeaux & LaBRI-CNRS)


This lecture can be viewed as a course on type theory with emphasis on Girard system F (intuitionistic quantified propositional logic) and its uses in formal semantics and pragmatics. It is designed for linguists and philosophers as well as for logicians and computer scientists interested in the modelling of human language. As opposed to the usual presentations of type theory, the syntax of type theory will be as brief as possible, but we shall give an account of the three levels of models, with what is known of their interrelations. The emphasis will be on denotational semantics a.k.a. categorical models.

Furthermore, these constructions will be seen at work on a selection of well-known or promising applications in formal semantics. The application to lexical semantics or pragmatics in a compositional setting will exemplify the logical contents. The later point on the dynamics of proofs and dialogue might be skipped is the time is too short (this depends on the attendants’ knowledge in linear logic).

Basic notions of mathematical logic and topology will help to follow the classes. Categorical notions will be introduced gently by examples when needed.

The actual contents (as in the slides below)

Course material

Further bibliography:

Backgound picture: (pale version of) an illustration by Max Ernst of some selected logical and poetic writtings of Lewis Carroll ("Wunderhorn").