Teaching

I taught a semester course on « Advanced Rewriting Theory » in the PhD student course at the Laboratory four Foundations of Computer Science in Edinburgh, during the academic year 1998-1999. The course was organized along the following topics:

Examples: term rewriting systems, lambda-calculus, call-by-value lambda-calculus, Petri nets, CCS, pi-calculus.

Basic concepts. Redexes, residuals, rewriting paths up to homotopy, Church-Rosser theorem expressed as a pushout property.

Standardization theorem. Standardization theorem and factorization theorems. Applications to an algebraic characterization of head-rewriting paths as universal cone (or spectrum) of a multi-adjunction.

Well orders. Higman and Kruskal theorems. Dershowitz recursive path orderings. A simple duality between Kruskal and Dershowitz. Applications to the Knuth-Bendix theorem.

Homology and applications to Rewriting Theory. Squier theorems. Existence of a finitely presentable and decidable monoid with no finite complete presentation.

I taught the course of « Advanced Rewriting Theory» at the DEA de Logique Mathématique et Fondements de l'Informatique de l'Université Paris 7, during the academic year 2000-2001. The DEA course was mainly expanding my previous course in Edinburgh. Partial lecture notes are available here.

I taught the course on « Games Semantics » at the DEA Programmation of the Université Paris 7, during the four academic years 2000-2004.

In June and July 2008, I taught an introductory course on « Quantum groupoids and tensorial logics » at the Ecole Doctorale de Science Mathématiques. A general description of the course appears here.

First course: a panoramic view on the course, with a logical prelude, an algebraic prelude, and a discussion on the converging point of the two fields. The slides of the course appear here.

Second course: categories, functors, transformations, natural transformations, sesqui-categories, 2-categories, formal theory of adjunctions, 2-category Rel. The slides of the course appear here.

Third course: monoidal categories, braidings, string diagrams, monoidal functors, functorial boxes, formal theory of monads, Kleisli and Eilenberg-Moore objects in 2-category. The slides of the course appear here.

Fourth course: Monoidal dualities, monoidal closed categories, star-autonomous categories, Frobenius objects, bicategory Span, monad homomorphisms, algebraic modules vs. categorical modules. The slides of the course appear here.

Fifth course: 2-monads, lax algebras of a 2-monad, monoidal categories, braidings, symmetries, lax monoidal categories, coherence theorems, a monoidal category of quadratic algebras and matrix calculus on the quantum plane, lax center of a monoidal category computed as a limit, Drinfeld's double construction.

Sixth course: Kan extensions, comma categories, Lawvere theories, operads, PROs, algebra of an operad, bicategory Span, presheaves,factorization systems, discrete fibrations and cofinal functors, free constructions by Kan extensions, application to the Kleisli and Eilenberg-Moore categories, homotopy limits seen as indexed limits.

I organize the course « Programming Languages Semantics » at the Master Parisien de Recherche en Informatique de l'Université Paris 7. The course is organized along three main topics:

Domain Theory. Lambda-calculus and recursion: the language PCF; Scott domains and continuity; Qualitative domains and stability; Qualitative domains with coherence and strong stability; logical relations and extensional collapse.

Category Theory. Categorical semantics of the lambda-calculus and of linear logic; cartesian closed categories and simply typed lambda-calculus; symmetric monoidal categories and linear logic; star-autonomous categories and classical duality; monads, monoids and duplication; 2-categories and formal theory of adjunctions.

Games Semantics. Dynamic models, and interpretation of programs as interactive strategies. Linear logic and duality between the Program and its Environment; arena games (Hyland, Ong, Nickau) vs. index games (Abramsky, Jagadeesan, Malacaria) ; Correspondence Syntax vs. Semantics: full abstraction theorems; PCF with control: interpretation of classical logic; PCF with local variables: interpretation of Idealized Algol; Well-bracketing, visibility and factorization theorems.

The slides and exercises (in French) of the course appear here.