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.

- Usual models, truth values, sheaves of usual models.
- Denotational semantics (categorical models).
- If time allows: dynamics of proof reductions / ludics

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).

- Foreword --- contents
- Propositional proof/type systems --- FOL in simple type theory
- Interlude: alternative interpretation of semantic representations (FOL formulae) in sheaf semantics
- Categorical interpretation of simply typed lambda calculus
- Second order lambda calculus -- quantified propositional proof system (Girard's system F)
- Quick reminder on the usual framework: Montague semantics
- System F based semantics and pragmatics
- Integrating facets in a compositional lexicon
- Categorical interpretation of system F quantified propositional intuitionistic calculus
- The logical syntax of (generalised) quantification and generics
- The Logical Syntax of Plurals
- Apology for system F
- Conclusion and perspective

- Slides:
- A freely available book: Jean-Yves GIRARD Proofs and types. Cambridge University Press 1989
- An early version of a JoLLI paper: Christian Bassac, Bruno Mery, Christian retoré Towards a Type-Theoretical Account of Lexical Semantics Journal of Logic, Language and Information. 19(2) pp. 229—245 2010 Preliminary version
- An early version of a paper in RLV: Christian Retoré Variable
types for meaning assembly: a logical syntax for
generic noun phrases introduced by "most"
*Recherches linguistiques de Vincennes 41:83--102 (2012)*Preliminary version. - Chapter three Montague semantics of the monograph:
**The logic of categorial grammars: a deductive account of natural language syntax and semantics (R. Moot & Ch. Retoré) july 2012 LNCS 6850** - Possibly the first two chapters of the aforementioned monograph.

- Nicholas ASHER
. Manuscript. http://timeml.org/jamesp/lexsemastypes-9.pdf*Lexical Meaning in Context: A Web of Words* - Christian BASSAC, Bruno MERY, Christian RETORE
Journal of Logic Language and Information 19(2) 2010.**Towards a Type-Theoretical Account of Lexical Semantics** - Francis CORBLIN
, PUF, 2004.*Théorie des représentations discursives* - L. T. F. GAMUT
r, Chicago University Press, 1991.*Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Gramma* - Jean-Yves GIRARD
Vol I & II. Hermann 2006. English version: The blind spot**Le point aveugle — cours de logique.** - Joachim LAMBEK & Phil SCOTT
Cambridge studies in advanced mathematics Cambridge University Press, 1988*Introduction to Higher-Order Categorical Logic* - Saunders MAC LANE & Ieke MOERDIJK
Springer University Texts, 1993**Sheaves in geometry and logic: a first introduction to topos theory** - Jean PETITOT,
Mathématiques et Sciences Humaines, 140, pp. 35-50, 1997**La neige est blanche ssi... Prédication et perception** - James PUSTEJOVSKY
MIT Press 1995.**The generative lexicon.** - François RECANATI
Folio essais, Gallimard, 2008.*Philosophie du langage (et de l'esprit)* - Anne Sjerp TROELSTRA & Dirk VAN DALEN
, North-Holland, 1988.*Constructivism in mathematics, Vol II*

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