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. [fichier pdf]
• 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]

Le mardi 15 janvier en salle Emmy Noether à partir de 8h30.

• 8h30 -- 9h Sven Meyer
  Grieg Friedman
  An elementary illustrated introduction to simplicial sets.


• 9h10 -- 9h40 Dhrubajyoti Ghosh
  Grieg Friedman
  An elementary illustrated introduction to simplicial sets.


• 9h50 -- 10h20 Loïc Chevalier
  Barnaby Hilken
  Towards a proof-theory of rewriting: the simply-typed 2-lambda-calculus.

Le vendredi 19 janvier en salle Bourbaki à partir de 17h.

• 17h -- 17h30 Simon Corbard
  Phil Wadler
  Theorem for free!


• 18h -- 18h30 Quentin Schroeder
  Peter Johnstone
  The point of pointless topology

Le mercredi 24 janvier

• 8h30 -- 9h Djamel Ait-Moussa
  Jean-Louis Krivine.
  Typed lambda-calculus in classical Zermelo-Frænkel set theory.


• 9h -- 9h30 Jean Caspar
  Paul Blain Levy
  Call-by-push-value: a subsuming paradigm


• 9h30 -- 10h Jonathan Baumann
  Martin Hofmann
  Syntax and Semantics of Dependent Types


• 10h -- 10h30 Adrien Mathieu
  Pierre-Louis Curien
  The Categorical Abstract Machine and Categorical Corbinators
  


• 14h -- 14h30 Titouan Quennet
  Samson Abramsky et Guy McCusker
  Game semantics


• 14h30 -- 15h Yee-Jian Tan
  Martin Hoffman
  Syntax and Semantics of Dependent Types

Le vendredi 26 janvier

• 10h30 -- 11h Léo Buisine
  Bojko Bakalov and Alexander Kirillov, Jr.
  Lectures on Tensor Categories and Modular Functors


• 11h -- 11h30 Felix Yvonnet
  Fosco Loregian
  Coend calculus the book


• 11h30 -- 12h Nicolas Nelson
  Arthan
  A traced monoidal category of relations.
  


• 11h -- 12h30 Rémy Kimbrough
  Peter Buneman, Shamim Naqvi, Val Tannen, Limsson Wong
  Principles of programming with complex objects and collection types

Le lundi 29 janvier

• 14h -- 14h30 Louis Milhaud
  Martin Hoffman
  Syntax and Semantics of Dependent Types


• 14h30 -- 15h Gurvan Debaussart
  Thérèse Hardin, Luc Maranget, Bruno Pagano
  Functional runtime systems within the Lambda-Sigma calculus


• 15h -- 15h30 Valeran Maytie
  Martin Hoffman
  Syntax and Semantics of Dependent Types

Le vendredi 2 février

• 9h -- 9h30 Hugo Peyraud-Magnin
  Yves Lafont et Alain Proutè
  Church-Rosser property and homology of monoids.


• 9h30 -- 10h Alexander Zenkovich
  Yves Lafont.
  Soft Linear Logic.

Le vendredi 16 février

• 14h -- 14h30 Simon Dima
  RAG Seely
  Locally Cartesian Closed Categories and Type Theory


• 14h30 -- 15h Vladimir Ivanov
  Patrick Cousot
  Types as Abstract Interpretations

Le lundi 19 février

• 9h -- 9h30 Edouard Nemery
  Paul-André Melliès
  The true concurrency of innocence


• 11h -- 11h30 Teiki Rigaud
  Samson Abramsky and Guy McCusker
  Game semantics

Le vendredi 22 mars

• 14h -- 14h30 Marie Tcheng


• 14h30 -- 15h Joseph Lenormand


• 15h -- 15h30 Anton Danilkin


• 15h30-- 16h Nassim Arifette

Diplôme de l'Ecole Normale Supérieure

Master Parisien de Recherche en Informatique

Paul-André Melliès

Samuel Mimram