Master Parisien de Recherche en Informatique
Lambda-calculs et catégories
Cours M1.20
Cours Magistral
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 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
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.
-
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]
Articles et pointeurs
A selection (always in development) of papers and surveys on the topic:
-
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]
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 mardi 1er février en ligne
9h30 Clotilde Bizière
Barnaby Hilken
Towards a proof-theory of rewriting: the simply-typed 2-lambda-calculus.
Le jeudi 3 février en ligne
10h -- Linda Gutsche
Samson Abramsky et Guy McCusker
Game semantics.
Le vendredi 4 février en ligne
11h30 -- Thomas Laure
Eugenio Moggi
Computational lambda-calculus and monads
Le mercredi 23 février en ligne
9:30 -- Lucas Larroque
Eugenio Moggi
Computational lambda-calculus and monads
Soutenances à venir
Marius Belly - Le Guilloux
Greg Friedman.
An elementary illustrated introduction to simplicial sets.
Théo Rudkiewicz
André Joyal
Une théorie combinatoire des séries formelles.
Baptiste Mouillon
Jaoslav Nesetril
Homomorphisms of structure (Concepts and highlights).
Hervé Sabrié
Noson S. Yanofsky
Computability and complexity of categorical structures
Quelques liens utiles