The course discusses recent developments in type-theoretic grammars with an emphasis on the syntax-semantics interface. Semantic interpretation in categorial type logics is realized in terms of the Curry-Howard correspondence between derivations and terms of the lambda calculus.

We start with the minimal requirements a categorial system has to meet in order to enjoy this correspondence.

We then turn to mismatches between syntactic and semantic organization,involving both overt and covert forms of movement. We discuss how these mismatches have been dealt with in multi-modal approaches (within the type-logical and the combinatory categorial grammar traditions), discontinuous calculi, lambda grammars. A shared property of these approaches is their reliance on non-logical axioms, which implies an essentially stipulative treatment of word order universals.

In the second part of the course, we turn to symmetric grammars, an extension of the typelogical framework originally proposed by Grishin in 1983. In the symmetric grammars, the familiar type-forming operations (product, slashes) are complemented with their duals (sum, difference operations). The two families interact via structure-preserving distributivity laws. Mismatches at the syntax-semantics interface are resolved in a way that respects word order and constituent structure.

Symmetric categorial grammar, from a logical point of view, has a`classical' flavour. The Curry-Howard correspondence for classical systems is expressed in terms of the $\lambda\mu$ calculus, and the continuation semantics that goes with it. We discuss current uses of continuations in natural language semantics.

In the final part, we discuss proof nets, parsing and complexity of the type logics we have considered, and their place within the Chomsky hierarchy.