Lecture one : general presentation, simply-typed lambda-calculus, elements of rewriting theory

Lecture two : categories and functors, natural transformations, the 2-category of categories, string diagrams

Lecture three : adjunctions, monads

Lecture four : finite developments, algebraic Church-Rosser theorem, event structures, asynchronous graphs

Lecture five : simply-typed lambda-calculus, cartesian closed categories, lambda-calculus with computational effects

Lecture six : limits and colimits, Kan extensions, monoids and mnemoids, semantics of local states, presheaf categories

Travaux Dirigés no 1 -- cartesian categories and monoids

Travaux Dirigés no 2 -- pullbacks, monos, epis and subobjects

Travaux Dirigés no 3 -- equalizers, epi-mono factorization, first-order logic

Travaux Dirigés no 4 -- multiset ordering, battle of the hydra, Higman and Kruskal theorems

Travaux Dirigés no 5 -- an equivalent formulation of adjunctions, application to cartesian and cartesian closed categorires

Travaux Dirigés no 6 -- distributivity laws between functors and monads, Grothendieck construction and set-theoretic colimits

• Jean-Yves Girard. Proofs and Types. [fichier pdf]
• Tom Leinster. Basic Category Theory. [fichier pdf]
• Paul-André Melliès. Categorical Semantics of Linear Logic. [fichier pdf]
• Peter Selinger. Lecture Notes on the Lambda-Calculus. [fichier pdf]

The n-Category Cafe

Homotopy Type Theory

• John Baez. Lectures on n-categories and cohomology. [fichier pdf]
• Audun Holme. Basic Modern Algebraic Geometry -- Introduction to Grothendieck's Theory of Schemes. [fichier pdf]
• Peter May. A concise course in algebraic topology. [fichier pdf]

• Samson Abramsky, Guy McCusker: game semantics. [fichier pdf]
• Samson Abramsky, Guy McCusker: linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. [fichier pdf]
• R. D. Arthan: a traced monoidal category of relations. [fichier pdf]
• Patrick Cousot: types as abstract interpretations. [fichier pdf]
• Pierre-Louis Curien: substitutions up to isomorphisms. [fichier pdf]
• Pierre-Louis Curien: category theory, a programming-language introduction. [fichier pdf]
• Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær: compiling monads. [fichier pdf]
• Marcelo Fiore, Nicola Gambino, Martin Hyland, Glynn Winskel: [fichier pdf]
• Daniel P. Friedman: from direct style to monadic style through continuation passing style. [fichier pdf]
• Daniel P. Friedman: direct style from monadic style and back. [fichier pdf]
• Greg Friedman: an elementary illustrated introduction to simplicial sets. [fichier pdf]
• Carsten Fuhrmann: direct models of the computational lambda-calculus. [fichier pdf]
• Nicola Gambino, Martin Hyland: well-founded trees and dependent polynomial functors. [fichier pdf]
• Richard Garner: two-dimensional models of type theory. [fichier pdf]
• Dan Ghica: geometry of synthesis. [fichier pdf]
• Thérèse Hardin, Luc Maranget, Bruno Pagano: functional runtime systems within the lambda-sigma calculus. [fichier pdf]
• Russ Harmer, Martin Hyland, Paul-André Melliès: categorical combinatorics for innocent strategies. [fichier pdf]
• Barnaby Hilken: towards a proof-theory of rewriting: the simply-typed 2-lambda-calculus. [fichier pdf]
• Peter Hines, Philip Scott: conditional quantum iteration from categorical traces. [fichier pdf]
• Martin Hofmann: Syntax and Semantics of Dependent Types [fichier pdf]
• Martin Hyland: the effective topos. [fichier pdf]
• Martin Hyland and John Power: the category theoretic understanding of universal algebra: Lawvere theories and monads. [fichier pdf]
• Martin Hyland, Paul Blain Levy, Gordon Plotkin, John Power: combining algebraic effects with continuations. [fichier pdf]
• André Joyal. Une théorie combinatoire des séries formelles. Advances in Mathematics, 42(1) :1 1981.
• André Joyal, Ross Street, Dominic Verity: traced monoidal categories. [fichier pdf]
• Joachim Kock: notes on polynomial functors. [fichier pdf]
• Jean-Louis Krivine: Typed lambda-calculus in classical Zermelo-Fraenkel set theory. [fichier pdf]
• Yves Lafont, Alain Prouté: Church-Rosser property and homology of monoids. [fichier pdf]
• Paul-André Melliès: functorial boxes in string diagrams. [fichier pdf]
• Paul-André Melliès: the true concurrency of innocence. [fichier pdf]
• Eugenio Moggi: computational lambda-calculus and monads. [fichier pdf]
• Luke Ong: on model-checking trees generated by higher-order recursion schemes. [fichier pdf]
• Andy Pitts: polymorphism is set-theoretic, constructively. [fichier pdf]
• Gordon Plotkin, John Power: computational effects determine monads. [fichier pdf] [erratum]
• RAG Seely: categorical semantics for higher order polymorphic lambda calculus. [fichier pdf]
• RAG Seely: modeling computations: a 2-categorical framework. [fichier pdf]
• Peter Selinger: Control categories and duality: on the categorical semantics of the lambda-mu calculus. [fichier pdf]
• Julianna Szido: le lambda-calcul vu comme monade initiale. [fichier pdf]
• Glynn Winskel, Mogens Nielsen: models for concurrency. [fichier pdf]

Lundi 9 janvier 2017 en salle U/V

Lundi 16 janvier 2017 en salle U/V

Lundi 16 janvier 2017 après-midi

Lundi 23 janvier 2017 en salle U/V

Lundi 23 janvier 2017 après-midi