Forthcoming lecture at ESSLLI 2012 in Opol

Proofs, models and categories for type theory,

with selected applications to natural language semantics

 

Christian Retoré (Université de Bordeaux, LaBRI-CNRS, INRIA)

 

This lecture can be viewed as a course on type theory (intuitionistic and linear, propositional, first order and higher order) and its uses in formal semantics. It 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.

                       
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 exemplifies all what will have been seen so far. 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 mathematical logic).

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

Bibliography:

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