Premier cours : lambda-calcul et 2-catégories [séances 1, 2 et 3]

Deuxième cours : diagrammes de cordes et adjonctions [séances 4 et 5]

Troisième cours : logique du second ordre et réalisabilité [séances 6 et 7]

Troisième cours (bis) : catégories monoidales

Quatrième cours : lambda-calcul simplement typé et catégories cartésiennes fermées

Cinquième cours : monoides et mnémoides, monades d'états globaux et locaux.

Sixième cours: lambda-calcul avec effets de bord, théorie formelle des monades.

Septième cours: distributeurs, constructions libres et monade d'états locaux

Huitième cours: fibrations et substitutions explicites

Travaux Dirigés no 1 -- produits cartésiens, action d'un monoide, ensembles simpliciaux.

Travaux Dirigés no 2 -- adjonctions, monade d'exception et monade de non-déterminisme.

Travaux Dirigés no 3 -- monade de non-déterminisme, monade engendrée par une adjonction, monades en Haskell, loi de distributivité entre monades.

Travaux Dirigés no 4 -- catégories cartésiennes fermées, lambda-calcul simplement typé, théorème du paramètre.

Travaux Dirigés no 5 -- catégories monoïdales, catégories monoïdales fermées.

• 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, 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: categorical semantics of linear logic. [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]
  
• Julianna Szido: le lambda-calcul vu comme monade initiale. [fichier pdf]
• Glynn Winskel, Mogens Nielsen: models for concurrency. [fichier pdf]

• 10h00 -- Wenjie Fang
  Barnaby Hilken. Towards a proof-theory of rewriting: the simply-typed 2-lambda-calculus.

• 9h30 -- Martin Gleize
  Eugenio Moggi. Computational lambda-calculus and monads.
  
  
• 10h30 -- Yi Dai
  Bart Jacobs. Simply Typed and Untyped Lambda Calculus Revisited
  
  
• 11h00 -- Pause
  
  
• 11h30 -- Antoine Toubhans
  Joachim Kock: note on polynomial functors.
  
  
• 12h00 -- Ludovic Patey
  Julianna Szido. Le lambda-calcul vu comme monade initiale.
  
  
• 14h00 -- Guillaume Brunerie
  Martin Hofmann. Syntax and Semantics of Dependent Types.
  
  
• 15h00 -- Charles-Pierre Astolfi
  Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær: compiling monads.
  
  
• 15h30 -- Aurélie Lagoutte
  Paul-André Melliès. Functorial boxes in string diagrams.
  
  
• 16h00 -- Nans Lefebvre
  R.D. Arthan. A traced monoidal category of relations.
  Paul-André Melliès. Functorial boxes in string diagrams.
  
  
• 16h30 -- Paul Brunet
  Paul-André Melliès. Categorical semantics of linear logic.
  
  
• 17h00 -- Alex Lang
  Caractéristique d'Euler d'une catégorie.

• 9h00 -- Emile Contal
  Martin Hofmann: Syntax and Semantics of Dependent Types.
  
  
• 9h30 -- Antoine Amarilli
  Paul-André Melliès. The true concurrency of innocence.
  
  
• 10h00 -- Pablo Rauzy
  Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær. Compiling monads.
  Daniel P. Friedman. From direct style to monadic style through continuation passing style.
  Daniel P. Friedman. Direct style from monadic style and back.
  
  
• 10h30 -- Floriane Dardard
  Guerino Mazzola. The topos of music.
  
  
• 11h00 -- Loredana Vamanu
  Samson Abramsky, Guy McCusker: game semantics.
  Russ Harmer, Martin Hyland, Paul-André Melliès. Categorical combinatorics for innocent strategies.
  
  
• 11h30 -- Raphael Cauderlier
  Richar Garner: two-dimensional models of type theory.
  
  
• 12h00 -- Guillaume Madelaine
  Samson Abramsky, Guy McCusker. Game semantics.
  Paul-André Melliès. The true concurrency of innocence.
  
  
• 12h30 -- Robin Morisset
  Patrick Cousot: types as abstract interpretations.
  Eugenio Moggi: computational lambda-calculus and monads.
  
  
• 14h00 -- Florence Clerc
  Paul-André Melliès. Categorical semantics of linear logic.
  Paul-André Melliès. Functorial boxes in string diagrams.
  
  
• 14h30 -- Samuel Bach
  Greg Friedman. An elementary illustrated introduction to simplicial sets.
  
  
• 15h00 -- Tie Cheng
  Thérèse Hardin, Luc Maranget, Bruno Pagano: functional runtime systems within the lambda-sigma calculus.

Diplôme de l'Ecole Normale Supérieure

Master Parisien de Recherche en Informatique

Paul-André Melliès

Samuel Mimram

The n-Category Café