Master Parisien de Recherche en Informatique

Lambda-calculs et catégories
Cours M1.20

Associahedre


Cours Magistral


Travaux Dirigés


Références bibliographiques du cours


Quelques pointeurs utiles sur la théorie des catégories

If you want to know more on the unifying role of category theory in various fields of mathematics and computer science, you are welcome to visit this dedicated blog: If you are interested in the recent connection between homotopy theory and type theory, a natural place to have a look at is this website: You may also have a look at these books.
Articles et pointeurs


A selection (always in development) of papers and surveys on the topic:

Calendrier des soutenances de cette année

Les soutenances en ligne ont lieu ici: Lien Zoom avec pour mot de passe: pi=314

Le mardi 4 janvier en salle Histoire, 45 rue d'Ulm, 2e étage, escalier D.

  • 14h -- 14h30 Oscar Fontaine
    Grieg Friedman
    An elementary illustrated introduction to simplicial set.

  • 14h30 -- 15h Juliette Schabanel
    André Joyal
    Une théorie combinatoire des séries formelles.

    • Le mercredi 5 janvier en salle Histoire, 45 rue d'Ulm, 2e étage, escalier D.

  • 14h -- 14h30 Francis Durand (exposé en ligne, Lien Zoom, mot de passe: pi=314)
    Samson Abramsky and Guy McCusker
    Game semantics.

  • 15h -- 15h30 Samuel Vivien
    Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær
    Compiling monads.

  • 15h30 -- 16h Paul Fournier
    Andrée Ehresmann and Jaime Gomez-Ramirez
    Conciliating neuroscience and phenomenology via category theory.

    • Le lundi 10 janvier en Amphi Galois

  • 9h30 -- 10h Tom Hubrecht
    Patrick Cousot
    Types as abstract interpretations.

  • 10h -- 10h30 Gabriel Doriath Döhler
    Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi
    Hints in unification.

  • 10h30 -- 11h Thomas Lamiaux
    Martin Hofmann
    Syntax and Semantics of Dependent Types.

    • Le mardi 11 janvier en salle Histoire, 45 rue d'Ulm, 2e étage, escalier D.

  • 14h -- 14h30 Arthur Léonard
    Yves Lafont et Alain Prouté
    Church-Rosser property and homology of monoids.

  • 14h30 -- 15h Gaia Carenini
    Mauro Jaskelioff and Eugenio Moggi
    Monad Transformers as Monoid Transformers.

  • 15h -- 15h30 Cyril Pujol
    Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi
    The calculus of signal Flow Diagrams I : Linear relations on streams

    • Le mercredi 12 janvier en ligne

  • 14h00 -- 14h30 Rémi Pallen
    Paul-André Melliès et Noam Zeilberger
    Functors are Type Refinement Systems.

    • Le lundi 17 janvier en Amphi Galois

  • 10h -- 10h30 Etienne Parcollet (en ligne sur Zoom avec pour mot de passe: pi=314)
    Jose Esperito Santo, Ralph Matthes et Luis Pinto
    Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search.

  • Pause de 10h30 à 11h

  • 11h -- 11h30 Neven Villani
    Ralf Jung, Jacques-Henri Jourdan, Robbet Krebbers, Derek Dreyer
    RustBelt: Securing the Foundations of the Rust Programming Language

  • 11h30 -- 12h Arnaud Daby-Seesaram
    Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Mogelberg, Andrew M. Pitt and Bas Spitters
    Modal dependent type theory and dependent right adjoints

  • Pause de 12h à 12h30

  • 12h30 -- 13h Victor Blanchi (en ligne sur Zoom avec pour mot de passe: pi=314)
    Paul-André Melliès
    Categorical Combinatorics of Scheduling and Synchronization in Game Semantics.

    • Le mercredi 19 janvier en salle Histoire, 45 rue d'Ulm, 2e étage, escalier D.

  • 10h -- 10h30 Léo Mangel
    Paige Randall North
    Towards a Directed Homotopy Type Theory

  • 10h30 -- 11h Nicolas Dumange
    Martin Hyland.
    Game semantics

  • 11h -- 11h30 Hector Buffière
    Thomas Colcombet et Daniela Petrisan
    Automata and minimisation

    • Le jeudi 27 janvier en ligne

  • 18h -- Linda Gutsche
    Samson Abramsky et Guy McCusker
    Game semantics.

  • 18h30 -- Thomas Laure
    Eugenio Moggi
    Computational lambda-calculus and monads

    • Le vendredi 28 janvier en ligne

  • 14h -- 14h30 Clotilde Bizière
    Barnaby Hilken
    Towards a proof-theory of rewriting: the simply-typed 2-lambda-calculus.

    • Soutenances à venir

  • Marius Belly - Le Guilloux
    Greg Friedman.
    An elementary illustrated introduction to simplicial sets.

  • Tom Hubrecht
    Patrick Cousot
    Types as abstract interpretations.

  • Lucas Larroque
    Eugenio Moggi
    Computational lambda-calculus and monads

  • Baptiste Mouillon
    Jaoslav Nesetril
    Homomorphisms of structure (Concepts and highlights).

  • Théo Rudkiewicz
    André Joyal
    Une théorie combinatoire des séries formelles.

  • Hervé Sabrié
    Noson S. Yanofsky
    Computability and complexity of categorical structures



    • Quelques liens utiles

    Diplôme de l'Ecole Normale Supérieure

    Master Parisien de Recherche en Informatique

    Paul-André Melliès

    Samuel Mimram